summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/bv-abstr-bug2.smt2
blob: 939439adf2cc3e9fb13c359f783d1af2d5041c19 (plain) 
1
2
3
4
5
6
7

; COMMAND-LINE: --solve-int-as-bv=32 --bitblast=eager
(set-logic QF_NIA)
(set-info :status sat)
(declare-fun _substvar_7_ () Bool)
(declare-fun _substvar_3_ () Int)
(assert (or _substvar_7_ (= 0 _substvar_3_)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback