1 files changed, 19 insertions, 12 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1f83bb547..ec37eaf26 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -46,8 +46,10 @@
 #include "theory/theory_engine.h"
 #include "theory/bv/theory_bv_rewriter.h"
 #include "proof/proof_manager.h"
+#include "main/options.h"
 #include "util/proof.h"
 #include "proof/proof.h"
+#include "proof/proof_manager.h"
 #include "util/boolean_simplification.h"
 #include "util/node_visitor.h"
 #include "util/configuration.h"
@@ -157,6 +159,8 @@ struct SmtEngineStatistics {
   IntStat d_numAssertionsPost;
   /** time spent in checkModel() */
   TimerStat d_checkModelTime;
+  /** time spent in checkProof() */
+  TimerStat d_checkProofTime;
   /** time spent in PropEngine::checkSat() */
   TimerStat d_solveTime;
   /** time spent in pushing/popping */
@@ -183,11 +187,11 @@ struct SmtEngineStatistics {
     d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
     d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
     d_checkModelTime("smt::SmtEngine::checkModelTime"),
+    d_checkProofTime("smt::SmtEngine::checkProofTime"),
     d_solveTime("smt::SmtEngine::solveTime"),
     d_pushPopTime("smt::SmtEngine::pushPopTime"),
     d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
     d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
-
  {
 
     StatisticsRegistry::registerStat(&d_definitionExpansionTime);
@@ -667,6 +671,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_decisionEngine(NULL),
   d_theoryEngine(NULL),
   d_propEngine(NULL),
+  d_proofManager(NULL),
   d_definedFunctions(NULL),
   d_assertionList(NULL),
   d_assignments(NULL),
@@ -696,6 +701,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_statisticsRegistry = new StatisticsRegistry();
   d_stats = new SmtEngineStatistics();
 
+  PROOF( d_proofManager = new ProofManager(); );
+
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
   d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic));
@@ -763,6 +770,7 @@ void SmtEngine::finishInit() {
   if(options::cumulativeMillisecondLimit() != 0) {
     setTimeLimit(options::cumulativeMillisecondLimit(), true);
   }
+
   PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); 
 }
 
@@ -777,16 +785,11 @@ void SmtEngine::finalOptionsAreSet() {
   }
 
   if(options::checkModels()) {
-    if(! options::produceModels()) {
-      Notice() << "SmtEngine: turning on produce-models to support check-model" << endl;
-      setOption("produce-models", SExpr("true"));
-    }
     if(! options::interactive()) {
-      Notice() << "SmtEngine: turning on interactive-mode to support check-model" << endl;
+      Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl;
       setOption("interactive-mode", SExpr("true"));
     }
   }
-
   if(options::produceAssignments() && !options::produceModels()) {
     Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl;
     setOption("produce-models", SExpr("true"));
@@ -3291,9 +3294,6 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
   finalOptionsAreSet();
   doPendingPops();
 
-
-  PROOF( ProofManager::currentPM()->addAssertion(ex); ); 
-
   Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl;
 
   if(d_queryMade && !options::incrementalSolving()) {
@@ -3308,6 +3308,8 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
     e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
     // Ensure expr is type-checked at this point.
     ensureBoolean(e);
+    // Give it to proof manager
+    PROOF( ProofManager::currentPM()->addAssertion(e); ); 
   }
 
   // check to see if a postsolve() is pending
@@ -3361,6 +3363,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
   // Check that UNSAT results generate a proof correctly.
   if(options::checkProofs()) {
     if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+      TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
       checkProof();
     }
   }
@@ -3384,9 +3387,10 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
 
   // Substitute out any abstract values in ex
   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
-
   // Ensure that the expression is type-checked at this point, and Boolean
   ensureBoolean(e);
+  // Give it to proof manager
+  PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); ); 
 
   // check to see if a postsolve() is pending
   if(d_needPostsolve) {
@@ -3437,6 +3441,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
   // Check that UNSAT results generate a proof correctly.
   if(options::checkProofs()) {
     if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+      TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
       checkProof();
     }
   }
@@ -3449,7 +3454,9 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
-  PROOF( ProofManager::currentPM()->addAssertion(ex);); 
+
+  PROOF( ProofManager::currentPM()->addAssertion(ex); ); 
+
   Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
 
   // Substitute out any abstract values in ex