diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-20 18:05:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-20 18:05:43 -0500 |
| commit | a0c5a51f6fae81ffeb1752ee4d75db7a51c23680 (patch) | |
| tree | 9f592a260c1dfe2cd311b0668ba6bd0ecd8d0713 /test/regress/regress1/quantifiers/dump-inst-i.smt2 | |
| parent | 34a4f78458773e9816d90c84fd2047b74a699527 (diff) | |
Add regressions that increase coverage (#2337)
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) |