blob: 6ac9048328c568be387cb35f674fb2a14646140d (
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
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --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 Int))
(
(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)
|
