blob: 2995f768249fc01f3c9f90e4d6cc70da5ad880b6 (
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
|
; REQUIRES: proof
; COMMAND-LINE: --dump-instantiations --proof
; EXPECT: unsat
; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)) )
; EXPECT: ( 2 )
; EXPECT: )
; EXPECT: (instantiations (forall ((x Int)) (or (not (S x)) (not (Q x))) )
; EXPECT: ( 2 )
; EXPECT: )
(set-logic UFLIA)
(set-info :status unsat)
(declare-fun P (Int) Bool)
(declare-fun Q (Int) Bool)
(declare-fun R (Int) Bool)
(declare-fun S (Int) Bool)
(declare-fun W (Int) Bool)
(declare-fun U (Int) Bool)
(assert (forall ((x Int)) (or (P x) (Q x))))
(assert (forall ((x Int)) (or (R x) (W x))))
(assert (forall ((x Int)) (or (S x) (U x))))
(assert (forall ((x Int)) (or (not (S x)) (not (Q x)))))
(assert (and (not (R 0)) (not (R 10)) (not (S 1)) (not (P 2))))
(assert (S 2))
; This tests that --proof minimizes the instantiations printed out.
; This regression should require only the 2 instantiations above, but
; may try more.
(check-sat)
|
