diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-14 17:06:14 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-14 17:06:14 +0000 |
commit | ce4ba524301ee3a8a297b2c3050e7d2c5ee58d08 (patch) | |
tree | 7b8896603bf711e2a45085defba0fd0ca63b54ed | |
parent | 8da791368c6d8cad97ff81b2b540c90ffdebc7ff (diff) |
restore destruction of stuff in driver
-rw-r--r-- | src/main/driver.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 24 |
2 files changed, 13 insertions, 13 deletions
diff --git a/src/main/driver.cpp b/src/main/driver.cpp index 36840f28e..00072d6d9 100644 --- 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 41d12b77d..747c92c0c 100644 --- 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); |