blob: e169e1a5ccb00e4ae83b0199d59b2b6e36c0f06a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status --decision=justification
(set-logic LIA)
(synth-fun P ((x Int) (y Int)) Bool
((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)
|
