summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus/issue3507.smt2
blob: aca7a61b0b76bf65415627acb258cc3084a9e524 (plain) 
1
2
3
4
5
6
7
8

; EXPECT: sat
; COMMAND-LINE: --sygus-inference --uf-ho
(set-logic ALL)
(declare-fun f (Int) Bool)
(declare-fun g (Int) Bool)
(assert (and (distinct f g) (g 0)))
(assert (exists ((x Int)) (f x)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback