blob: 9221a2abcd1cf86e93e42b27da28615d6977b694 (
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: --dump-instantiations --incremental
; SCRUBBER: sed -e 's/skv_.* )$/skv_TERM )/'
; EXPECT: unsat
; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) )
; EXPECT: ( skv_TERM )
; EXPECT: )
; EXPECT: (instantiation (forall ((x Int)) (P x) )
; EXPECT: ( skv_TERM )
; EXPECT: )
; EXPECT: unsat
; EXPECT: (skolem (forall ((x Int)) (or (P x) (R x)) )
; EXPECT: ( skv_TERM )
; EXPECT: )
; EXPECT: (instantiation (forall ((x Int)) (P x) )
; EXPECT: ( skv_TERM )
; EXPECT: )
(set-logic UFLIA)
(declare-fun P (Int) Bool)
(declare-fun Q (Int) Bool)
(assert (forall ((x Int)) (P x)))
(push 1)
(assert (exists ((x Int)) (and (not (P x)) (not (Q x)))))
(check-sat)
(pop 1)
(declare-fun R (Int) Bool)
(assert (exists ((x Int)) (and (not (P x)) (not (R x)))))
(check-sat)
|
