blob: bad1964c2965b567e598c3c76228c49912820294 (
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
|
; COMMAND-LINE: --incremental --simplification=none
; EXPECT: sat
; EXPECT: unsat
(set-logic QF_UFLIA)
(declare-fun base () Int)
(declare-fun n () Int)
(declare-fun g (Int) Bool)
(declare-fun f (Int) Bool)
(push 1)
(assert (<= 0 n))
(assert (f n))
(assert (= (f n) (or (= (- n base) 1) (g n))))
(check-sat)
(pop 1)
(push 1)
(assert (<= 0 n))
(assert (or (= (- n base) 1) (g n)))
(assert (not (g n)))
(assert (= base (- 2)))
(check-sat)
(pop 1)
|
