diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-10 23:03:43 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-10 23:03:43 -0700 |
| commit | 8e16da7e154dbd22ca05b769bc0ceb841b9ae513 (patch) | |
| tree | 6035174e5ca7f228b3c9b0286dd6dfa620c0dd9c | |
| parent | 6a2619c8c14e138b0ce4fdfe59e06dbcde2f61c7 (diff) | |
reset-assertions: Update TheoryEngine's PropEngine*
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.
| -rw-r--r-- | src/smt/smt_engine.cpp | 1 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 4 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 |
3 files changed, 4 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bfb126e9e..5b5504cc5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5594,6 +5594,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 62c9c87b1..920fdfbdb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -897,6 +897,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 |