diff options
Diffstat (limited to 'test/regress/regress1/quantifiers/dump-inst-i.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/dump-inst-i.smt2 | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/dump-inst-i.smt2 b/test/regress/regress1/quantifiers/dump-inst-i.smt2 new file mode 100644 index 000000000..9221a2abc --- /dev/null +++ b/test/regress/regress1/quantifiers/dump-inst-i.smt2 @@ -0,0 +1,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) |