diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-27 16:37:14 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-27 16:37:14 -0700 |
| commit | 97f1e4592b617a5682a8e990b4f82d3cbb6ee037 (patch) | |
| tree | 802d51af8b5d86e7d62e56eea8976ff6e8f0f533 /test | |
| parent | ea1f107a92f22961a50fbc51d93780f89cbd66e0 (diff) | |
Fix issues with unsat cores and reset-assertions (#4159)
Fixes #4151. Commit e9f4cec2cad02e270747759223090c16b9d2d44c fixed how
`(reset-assertions)` is handled by destroying and recreating the
`PropEngine` owned by `SmtEngine`. When unsat cores are enabled,
creating a `PropEngine` triggers the creation of a SAT proof and a CNF
proof. In the `ProofManager`, we had assertions that checked that those
kinds of proofs were only created once, which is not true anymore. This
commit removes the assertions, cleans up the memory management in
`ProofManager` to use `std::unique_ptr` and makes all the
`ProofManager::init*` methods non-static for consistency.
The commit also fixes an additional issue that I encountered while
testing the fix: When creating the new `PropEngine`, we were not
asserting `true` and `(not false)`, which lead to an error if we tried
to get the unsat core after a `(reset-assertion)` command and we had
asserted `(assert false)`. The commit fixes this by asserting `true` and
`(not false)` in the constructor of `PropEngine`.
The regression test is an extension of the example in #4151 and covers
both issues.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/smtlib/issue4151.smt2 | 13 |
2 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8382e40fc..a5acd62fb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -902,6 +902,7 @@ set(regress_0_tests regress0/smtlib/global-decls.smt2 regress0/smtlib/issue4028.smt2 regress0/smtlib/issue4077.smt2 + regress0/smtlib/issue4151.smt2 regress0/smtlib/reason-unknown.smt2 regress0/smtlib/reset.smt2 regress0/smtlib/reset-assertions1.smt2 diff --git a/test/regress/regress0/smtlib/issue4151.smt2 b/test/regress/regress0/smtlib/issue4151.smt2 new file mode 100644 index 000000000..629ec48b6 --- /dev/null +++ b/test/regress/regress0/smtlib/issue4151.smt2 @@ -0,0 +1,13 @@ +; EXPECT: sat +; EXPECT: unsat +; EXPECT: ( +; EXPECT: ) +(set-logic ALL) +(set-option :incremental true) +(set-option :produce-unsat-assumptions true) +(set-option :produce-unsat-cores true) +(check-sat) +(reset-assertions) +(assert false) +(check-sat) +(get-unsat-core) |