summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus/pbe-pred-contra.sy
blob: 22fc12e60a9bf1142d9722d327abf5f8c938d92a (plain) 
1
2
3
4
5
6
7

; COMMAND_LINE: --cegqi-si=none --sygus-out=status
; EXPECT: unknown
(set-logic LIA)
(synth-fun P ((x Int)) Bool)
(constraint (P 54))
(constraint (not (P 54)))
(check-synth)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback