diff options
Diffstat (limited to 'src/smt/smt_solver.cpp')
| -rw-r--r-- | src/smt/smt_solver.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 3f663726c..fbb21034a 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -65,7 +65,11 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) { theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id); } - + // Add the proof checkers for each theory + if (d_pnm) + { + d_theoryEngine->initializeProofChecker(d_pnm->getChecker()); + } Trace("smt-debug") << "Making prop engine..." << std::endl; /* force destruction of referenced PropEngine to enforce that statistics * are unregistered by the obsolete PropEngine object before registered |