3 files changed, 12 insertions, 0 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c9d0b95b5..f74e52509 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -102,7 +102,10 @@ PropEngine::PropEngine(TheoryEngine* te,
   PROOF (
          ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
          );
+}
 
+void PropEngine::finishInit()
+{
   NodeManager* nm = NodeManager::currentNM();
   d_cnfStream->convertAndAssert(nm->mkConst(true), false, false, RULE_GIVEN);
   d_cnfStream->convertAndAssert(
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 7f1d5ef65..9a2daee49 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -70,6 +70,13 @@ class PropEngine
   CVC4_PUBLIC ~PropEngine();
 
   /**
+   * Finish initialize. Call this after construction just before we are
+   * ready to use this class. Should be called after TheoryEngine::finishInit.
+   * This method converts and asserts true and false into the CNF stream.
+   */
+  void finishInit();
+
+  /**
    * This is called by SmtEngine, at shutdown time, just before
    * destruction.  It is important because there are destruction
    * ordering issues between some parts of the system (notably between
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index e0837c7cf..a31d84587 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -77,6 +77,7 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
   d_theoryEngine->setPropEngine(getPropEngine());
   Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
   d_theoryEngine->finishInit();
+  d_propEngine->finishInit();
 }
 
 void SmtSolver::resetAssertions()
@@ -92,6 +93,7 @@ void SmtSolver::resetAssertions()
   // Notice that we do not reset TheoryEngine, nor does it require calling
   // finishInit again. In particular, TheoryEngine::finishInit does not
   // depend on knowing the associated PropEngine.
+  d_propEngine->finishInit();
 }
 
 void SmtSolver::interrupt()