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

; EXPECT: unsat
; COMMAND-LINE: --sygus-inference --sygus-qe-preproc --no-check-unsat-cores
(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