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

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