summaryrefslogtreecommitdiff
path: root/test/regress/regress0/nl/issue3991.smt2
blob: c006b288580721783ec52f3933e4a925d1d5a096 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13

; COMMAND-LINE: --incremental --check-unsat-cores
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
(set-logic QF_NIA)
(declare-const i7 Int)
(check-sat)
(declare-const v18 Bool)
(assert (and (= i7 93) (or (> 19 i7) v18) v18))
(check-sat)
(assert (> 19 i7))
(assert (> (div i7 0) 0))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback