diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-13 13:24:43 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-13 13:24:43 -0700 |
| commit | ca65101e2d56a476367c8ad09b416b66403be7a7 (patch) | |
| tree | f0217edeee991073146d7d681cdf64c6c3476f22 /test | |
| parent | c369afa180b7cb3d9388c39d18fcb81e8246ff21 (diff) | |
Properly clean up assertion stack in CnfProof (#2147)
Fixes issue #2137. CnfProof has a stack of assertions that are being
converted to clauses. Previously, it could happen that while an
assertion was being added, TheoryProxy::explainPropagation() would be
called from Solver::reason() and push an assertion to the stack that was
then not removed. This lead to a clause id of the assertion being
associated with the explanation instead, which in turn could lead to a
wrong unsat core. This commit identifies two cases where
TheoryProxy::explainPropagation() is called without cleaning up the
assertion stack afterwards. It also adds an assertion that the assertion
stack must be empty when we are getting the unsat core.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress0/push-pop/issue2137.min.smt2 | 11 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 3c02ea13c..377e91897 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -580,6 +580,7 @@ REG0_TESTS = \ regress0/push-pop/inc-double-u.smt2 \ regress0/push-pop/incremental-subst-bug.cvc \ regress0/push-pop/issue1986.smt2 \ + regress0/push-pop/issue2137.min.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/issue2137.min.smt2 b/test/regress/regress0/push-pop/issue2137.min.smt2 new file mode 100644 index 000000000..372e8f1f3 --- /dev/null +++ b/test/regress/regress0/push-pop/issue2137.min.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --incremental --check-unsat-cores +; EXPECT: sat +; EXPECT: unsat +(set-logic ALL) +(declare-fun a () Real) +(declare-fun b () Bool) +(assert (< 0 a)) +(assert (xor b (< 0 a 0) false)) +(check-sat) +(assert (not b)) +(check-sat) |