summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uflia/check04.smt2
blob: 61bc8a5d6ac8176ae9418bc9070314dc718d0e07 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

(set-logic QF_LIA)
(declare-fun _b () Int)
(declare-fun _n () Int)
(declare-fun _x () Bool)

(assert (<= 2 _n))
(assert  (not (= _b 0)))

(push 1)
(assert (or (= _n 1) (or _x (= _b 0))))
(check-sat)
(pop 1)

(assert (or (= _n 1) (or _x (= _b 0))))

(assert (or (not _x) (= _n 1)))

(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback