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

; EXPECT: sat
; COMMAND-LINE: --sygus-inference --uf-ho --quiet
(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