restore destruction of stuff in driver

diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index 36840f28e9bc65e368431e82941df7f297f2bc18..00072d6d9fbb47b1b626232b0a7987e4df712692 100644 (file)
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -326,7 +326,7 @@ int runCvc4(int argc, char* argv[], Options& options) {
     pStatistics->flushInformation(*options.err);
   }
 
-  exit(returnValue);
+  return returnValue;
 }
 
 /** Executes a command. Deletes the command after execution. */

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 41d12b77dff95489590d2e9bee0c24e63cfacceb..747c92c0ce58f598229e977e8f3ee8333665c562 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -283,6 +283,18 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   StatisticsRegistry::registerStat(&d_numAssertionsPre);
   StatisticsRegistry::registerStat(&d_numAssertionsPost);
 
+  // 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, const_cast<const LogicInfo&>(d_logic));
+
+  // Add the theories
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+    d_theoryEngine->addTheory<theory::TheoryTraits<THEORY>::theory_class>(THEORY);
+  CVC4_FOR_EACH_THEORY;
+
   // global push/pop around everything, to ensure proper destruction
   // of context-dependent data structures
   d_userContext->push();
@@ -316,18 +328,6 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
 }
 
 void SmtEngine::finishInit() {
-  // 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, const_cast<const LogicInfo&>(d_logic));
-
-  // Add the theories
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-    d_theoryEngine->addTheory<theory::TheoryTraits<THEORY>::theory_class>(THEORY);
-  CVC4_FOR_EACH_THEORY;
-
   d_decisionEngine = new DecisionEngine(d_context, d_userContext);
   d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
   d_theoryEngine->setPropEngine(d_propEngine);