blob: 4dd7268750b1fce0d1a497abfc4463adb094caca (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic LIA)
(
synth-fun f_143-17-143-55 ( (x2 Int) (x1 Int) (parentNode Int) (EMPTY_PARENT Int)) Bool
((Start Bool (
(< IntExpr IntExpr)
(and Start Start)
(= IntExpr IntExpr)
(not Start )
(<= IntExpr IntExpr)
(or Start Start)
))
(IntExpr Int (
x2 x1 parentNode EMPTY_PARENT
0 1
))
)
)
(declare-var x2_143-17-143-55 Int)
(declare-var x1_143-17-143-55 Int)
(declare-var parentNode_143-17-143-55 Int)
(declare-var EMPTY_PARENT_143-17-143-55 Int)
(constraint (=> (and (= parentNode_143-17-143-55 0) (and (= EMPTY_PARENT_143-17-143-55 -1) (and (= x2_143-17-143-55 1) (= x1_143-17-143-55 1)) ) ) (= (f_143-17-143-55 x2_143-17-143-55 x1_143-17-143-55 parentNode_143-17-143-55 EMPTY_PARENT_143-17-143-55 ) true)))
(check-synth)
|
