1 files changed, 5 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index caa757426..7f9658ba0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -692,8 +692,6 @@ 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));
@@ -716,6 +714,9 @@ void SmtEngine::finishInit() {
   // ensure that our heuristics are properly set up
   setDefaults();
 
+  Assert(d_proofManager == NULL);
+  PROOF( d_proofManager = new ProofManager(); );
+
   d_decisionEngine = new DecisionEngine(d_context, d_userContext);
   d_decisionEngine->init();   // enable appropriate strategies
 
@@ -1366,8 +1367,8 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  if (options::incrementalSolving() && options::proof()) {
-    Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof" << endl;
+  if(options::incrementalSolving() && (options::proof() || options::unsatCores())) {
+    Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof or --produce-unsat-cores, try --tear-down-incremental instead)" << endl;
     setOption("incremental", SExpr("false"));
   }
 }