diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-02 17:45:04 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-02 17:45:04 -0700 |
| commit | be58c8ead1d36ab3625faf848b2ebdce8d5de8a9 (patch) | |
| tree | c35ba7d793543ee88cdcc23ca0a892afc758eb26 | |
| parent | be08eae24750b006d8a4b1e27e0e242553f64735 (diff) | |
Add regression test for issue #1986 (#2114)
The issue is not triggered anymore after PR #2059 but the test case is
good to have for changes in MiniSat code.
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress0/push-pop/issue1986.smt2 | 22 |
2 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 1866cf9f4..3c02ea13c 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -579,6 +579,7 @@ REG0_TESTS = \ regress0/push-pop/inc-define.smt2 \ regress0/push-pop/inc-double-u.smt2 \ regress0/push-pop/incremental-subst-bug.cvc \ + regress0/push-pop/issue1986.smt2 \ regress0/push-pop/quant-fun-proc-unfd.smt2 \ regress0/push-pop/simple_unsat_cores.smt2 \ regress0/push-pop/test.00.cvc \ diff --git a/test/regress/regress0/push-pop/issue1986.smt2 b/test/regress/regress0/push-pop/issue1986.smt2 new file mode 100644 index 000000000..b1594ef2e --- /dev/null +++ b/test/regress/regress0/push-pop/issue1986.smt2 @@ -0,0 +1,22 @@ +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic SAT) +(set-option :incremental true) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v5 () Bool) +(check-sat) +(push) +(assert (or (and (or true v1) (and (and (or v1 v1) true) true)) (or v2 (and v2 false)))) +(check-sat) +(assert (or (and (and v3 (and (or v4 v3) (and v1 false))) (and (and (or v2 true) v5) (and (and false v1) true))) v3)) +(push) +(pop) +(pop) +(assert true) +(push) +(assert (and (or v4 v5) true)) +(check-sat) |