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 /test/regress/regress0 | |
| 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.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/push-pop/issue1986.smt2 | 22 |
1 files changed, 22 insertions, 0 deletions
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) |