blob: 38e60d4db36501c1912a31d3eca00e7f836267e3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
; COMMAND-LINE: --dump-instantiations
; 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: )
(set-logic UFLIA)
(set-info :status unsat)
(declare-fun P (Int) Bool)
(declare-fun Q (Int) Bool)
(assert (forall ((x Int)) (P x)))
(assert (exists ((x Int)) (and (not (P x)) (not (Q x)))))
(check-sat)
|
