reset-assertions: Update TheoryEngine's PropEngine* (#4032)

Fixes #4028. TheoryEngine's pointer was not updated to the new
PropEngine when resetting assertions. This commit fixes that. As far
as I can tell, this was the only class storing a PropEngine* that
isn't owned by PropEngine, so we should hopefully not have other
similar issues.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e4e582b6e4df0a64cd06073f90f566939aa790b8..27d06e1042873cdfdef9d7b2307af103b19d97f1 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5588,6 +5588,7 @@ void SmtEngine::resetAssertions()
                                     d_userContext,
                                     d_private->getReplayLog(),
                                     d_replayStream));
+  d_theoryEngine->setPropEngine(getPropEngine());
 }
 
 void SmtEngine::interrupt()

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e8223f1a13352316f55b09006d697289b33df781..c1e1e4cac621815f700f9d915b14c07b172232bf 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -496,8 +496,8 @@ class TheoryEngine {
                                               d_logicInfo);
   }
 
-  inline void setPropEngine(prop::PropEngine* propEngine) {
-    Assert(d_propEngine == NULL);
+  void setPropEngine(prop::PropEngine* propEngine)
+  {
     d_propEngine = propEngine;
   }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 47290467d95ee8c9c59fa62e3310d6d1f89d79ec..691791732f472c541b84bae86a6c6ec1e4b548d2 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -898,6 +898,7 @@ set(regress_0_tests
   regress0/smt2output.smt2
   regress0/smtlib/get-unsat-assumptions.smt2
   regress0/smtlib/global-decls.smt2
+  regress0/smtlib/issue4028.smt2
   regress0/smtlib/reason-unknown.smt2
   regress0/smtlib/reset-assertions1.smt2
   regress0/smtlib/reset-assertions2.smt2

diff --git a/test/regress/regress0/smtlib/issue4028.smt2 b/test/regress/regress0/smtlib/issue4028.smt2
new file mode 100644 (file)
index 0000000..3d2f8b5
--- /dev/null
+++ b/test/regress/regress0/smtlib/issue4028.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental true)
+(push 3)
+(check-sat)
+(reset-assertions)
+(push 4)
+(check-sat)