blob: e4503ba1d39e65f041c04697f10971e767a42a70 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: unsat
(set-logic QF_UFLIA)
(declare-fun _n () Int)
(declare-fun _f (Int) Bool)
(declare-fun _g (Int) Bool)
(assert (not (= _n 0)))
(push 1)
(assert (or (_g 1) (or (not (_g _n)) (not (_f _n)))))
(check-sat)
(pop 1)
(assert
(or (and (_g _n) (_f _n))
(not (or (not (_g _n)) (not (_f _n))))))
(assert (or (not (_g _n)) (not (_g 0))))
(assert (or (not (_g _n)) (_g 0)))
(check-sat)
|
