summaryrefslogtreecommitdiff
path: root/test/regress/regress0/int-to-bv/overflow.smt2
blob: 30e47adb330c0dd720d45ff552f77733fca5930a (plain) 
1
2
3
4
5
6
7
8
9

; COMMAND-LINE: --solve-int-as-bv=4
; EXPECT: unknown
(set-logic QF_NIA)
(declare-const x Int)
(declare-const y Int)
(assert (= (- 1) (+ x y)))
(assert (> x 0))
(assert (> y 0))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback