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.

1 files changed, 0 insertions, 3 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 299cc357b..30c1cd0f5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1017,9 +1017,6 @@ void SmtEngine::finalOptionsAreSet() {
 
   d_fullyInited = true;
   Assert(d_logic.isLocked());
-
-  d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(true));
-  d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(false).notNode());
 }
 
 void SmtEngine::shutdown() {