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

; COMMAND-LINE: --solve-int-as-bv=32 
(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