From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 11 Mar 2020 18:57:22 +0000 (-0700)
Subject: reset-assertions: Update TheoryEngine's PropEngine* (#4032)
X-Git-Tag: cvc5-1.0.0~3511
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=05dc596e5b9ef9d4c45e2fa92a56ef1ec2aede76;p=cvc5.git

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 e4e582b6e..27d06e104 100644
--- 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 e8223f1a1..c1e1e4cac 100644
--- 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 47290467d..691791732 100644
--- 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
index 000000000..3d2f8b52b
--- /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)