From 7edd9eb6ecf8d36beea059a62ce573fdb6a6f8a1 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 30 Sep 2014 16:58:24 -0400
Subject: [PATCH] Proofs- and cores-related segfault fixes (mainly a usability
 issue), thanks Christoph Sticksel for reporting these.

---
 src/main/driver_unified.cpp  | 11 ++---------
 src/main/options             |  2 +-
 src/options/mkoptions        |  4 ++++
 src/smt/smt_engine.cpp       |  9 +++++----
 src/theory/theory_engine.cpp |  4 ++--
 5 files changed, 14 insertions(+), 16 deletions(-)

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 1202c7882..bf297ad9e 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -268,15 +268,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     Command* cmd;
     bool status = true;
     if(opts[options::interactive] && inputFromStdin) {
-      if(opts[options::tearDownIncremental] && opts[options::incrementalSolving]) {
-        if(opts.wasSetByUser(options::incrementalSolving)) {
-          throw OptionException("--tear-down-incremental incompatible with --incremental");
-        }
-
-        cmd = new SetOptionCommand("incremental", false);
-        cmd->setMuted(true);
-        pExecutor->doCommand(cmd);
-        delete cmd;
+      if(opts[options::tearDownIncremental]) {
+        throw OptionException("--tear-down-incremental doesn't work in interactive mode");
       }
 #ifndef PORTFOLIO_BUILD
       if(!opts.wasSetByUser(options::incrementalSolving)) {
diff --git a/src/main/options b/src/main/options
index b9262bfa4..6cc6a0ca0 100644
--- a/src/main/options
+++ b/src/main/options
@@ -52,7 +52,7 @@ option segvSpin --segv-spin bool :default false
  spin on segfault/other crash waiting for gdb
 undocumented-alias --segv-nospin = --no-segv-spin
 
-expert-option tearDownIncremental --tear-down-incremental bool :default false
+expert-option tearDownIncremental : --tear-down-incremental bool :default false
  implement PUSH/POP/multi-query by destroying and recreating SmtEngine
 
 expert-option waitToJoin --wait-to-join bool :default true
diff --git a/src/options/mkoptions b/src/options/mkoptions
index a3a1571ec..03d7837ac 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -352,6 +352,10 @@ function handle_option {
       WARN "$internal is inaccessible via SmtEngine (no smt name for option) but can be set via command-line: $long_option $short_option $long_option_alternate $short_option_alternate"
     fi
   fi
+  # in options files, use an smt name of ":" to force there not to be one
+  if [ "$smtname" = : ]; then
+    smtname=
+  fi
 
   # check for duplicates
   if [ "$internal" != - ]; then
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"));
   }
 }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 073f2ab94..01387637e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -65,6 +65,8 @@ using namespace CVC4;
 using namespace CVC4::theory;
 
 void TheoryEngine::finishInit() {
+  PROOF (ProofManager::initTheoryProof(); );
+
   // initialize the quantifiers engine
   d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
 
@@ -170,8 +172,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 
-  PROOF (ProofManager::initTheoryProof(); );
-
   d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
 
   StatisticsRegistry::registerStat(&d_arithSubstitutionsAdded);
-- 
2.30.2