diff options
Diffstat (limited to 'src/smt/smt_solver.cpp')
| -rw-r--r-- | src/smt/smt_solver.cpp | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index c64689be6..922831106 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -51,7 +51,8 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) d_smt.getUserContext(), d_rm, d_pp.getTermFormulaRemover(), - logicInfo)); + logicInfo, + d_smt.getOutputManager())); // Add the theories for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; @@ -65,8 +66,11 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) * are unregistered by the obsolete PropEngine object before registered * again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine( - d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm)); + d_propEngine.reset(new PropEngine(d_theoryEngine.get(), + d_smt.getContext(), + d_smt.getUserContext(), + d_rm, + d_smt.getOutputManager())); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -82,8 +86,11 @@ void SmtSolver::resetAssertions() * statistics are unregistered by the obsolete PropEngine object before * registered again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine( - d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm)); + d_propEngine.reset(new PropEngine(d_theoryEngine.get(), + d_smt.getContext(), + d_smt.getUserContext(), + d_rm, + d_smt.getOutputManager())); d_theoryEngine->setPropEngine(getPropEngine()); // Notice that we do not reset TheoryEngine, nor does it require calling // finishInit again. In particular, TheoryEngine::finishInit does not |