summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers/issue5279-nqe.smt2
blob: b87f36ebecc014c6690efd3c613665d1b13380e4 (plain) 
1
2
3
4
5

(set-logic LIA)
(set-option :cegqi-nested-qe true)
(set-info :status unsat)
(assert (forall ((a Int) (b Bool)) (= a (ite b 0 1))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback