From be58c8ead1d36ab3625faf848b2ebdce8d5de8a9 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 2 Jul 2018 17:45:04 -0700
Subject: [PATCH] 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.
---
 test/regress/Makefile.tests                   |  1 +
 test/regress/regress0/push-pop/issue1986.smt2 | 22 +++++++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 test/regress/regress0/push-pop/issue1986.smt2

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)
-- 
2.30.2