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.

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 1866cf9f4f97a2ad1ebcca2f36dcbc879e37abfc..3c02ea13cd67201450b1e6b32dffc2af5247a5a5 100644 (file)
--- 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 (file)
index 0000000..b1594ef
--- /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)