blob: daa3ca417809f5bf9caf4f9c0d755f8e1539d263 (
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
29
30
31
32
33
34
35
36
37
|
; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: unsat
(set-logic QF_UFLIA)
(declare-fun b () Int)
(declare-fun n () Int)
(declare-fun f (Int) Bool)
(declare-fun g (Int) Bool)
(assert (<= 0 n))
(push 1)
(assert (or (g (- 1)) (= b 0)))
(assert (or (= (- n b) 1) (not (or (= (- n b) 1) (f (- n 2))))))
(check-sat)
(pop 1)
(push 1)
(assert (or (g (- n 1)) (= n b)))
(assert (or (not (f n)) (not (= n b))))
(assert (not (f (- n 2))))
(assert (or (not (g (- n 1))) (not (= (- n b) 1))))
(assert (or (not (g (- n 1))) (or (= (- n b) 1) (f (- n 2)))))
(assert (or (f n) (and (not (f n)) (f n))))
(check-sat)
(pop 1)
|
