diff options
-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) |