summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus/issue4009-qep.smt2
blob: 71b9f20bd6937031310f8cd85d40367125a6c948 (plain) 
1
2
3
4
5
6
7

; EXPECT: unsat
; COMMAND-LINE: --sygus-inference --sygus-qe-preproc -q
(set-logic ALL)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ((c Real)) (and (xor (> c a) (= b 0)) (distinct (+ a b) 0))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback