blob: d593a7d9e661a1e1ed59404bf2f2122db259ffd5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification
(set-logic LIA)
(synth-fun P ((x Int) (y Int)) Bool
((Start Bool) (StartIntC Int) (StartInt Int))
((Start Bool ((and Start Start)
(not Start)
(<= StartInt StartIntC)
(<= StartInt StartInt)
(>= StartInt StartInt)
(<= StartIntC StartInt)
(>= StartIntC StartInt)
(<= StartIntC StartIntC)
))
(StartIntC Int (0 0 1))
(StartInt Int (x y 0 1))))
(constraint (P 0 2))
(check-synth)
|