diff options
Diffstat (limited to 'test/regress/regress1/quantifiers/dump-inst-proof.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/dump-inst-proof.smt2 | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 new file mode 100644 index 000000000..c4eedc16f --- /dev/null +++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --dump-instantiations --proof +; EXPECT: unsat +; EXPECT: (instantiation (forall ((x Int)) (or (P x) (Q x)) ) +; EXPECT: ( 2 ) +; EXPECT: ) +; EXPECT: (instantiation (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) |