summaryrefslogtreecommitdiff
path: root/test/regress/regress0/push-pop/bug233.cvc.smt2
blob: 422f8d5ca32f02ce57ee1d36faf73217bb2b9a63 (plain) 
1
2
3
4
5
6
7
8

; COMMAND-LINE: --incremental
; EXPECT: unsat
; EXPECT: sat
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(check-sat-assuming ( (not (let ((_let_1 (and a b))) (or _let_1 (not _let_1)))) ))
(check-sat-assuming ( (not (or a b)) ))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback