This commit:

* enables decision heuristic (justification) for QF_BV and QF_AUFBV
* disables a failing regression in aufbv (because of equality engine
  assert failure trigerred by above change)
* moves around the init procedure smt_engine
* destruction time issues because of moving this -- still to be fixed,
  currently get around by not destucting stuff in driver

1 files changed, 11 insertions, 3 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index b38b3c1e0..937099e38 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -27,7 +27,7 @@ using namespace std;
 
 namespace CVC4 {
 
-  DecisionEngine::DecisionEngine(context::Context *sc,
+DecisionEngine::DecisionEngine(context::Context *sc,
                                  context::Context *uc) :
   d_enabledStrategies(),
   d_needIteSkolemMap(),
@@ -37,11 +37,18 @@ namespace CVC4 {
   d_satSolver(NULL),
   d_satContext(sc),
   d_userContext(uc),
-  d_result(sc, SAT_VALUE_UNKNOWN)
+  d_result(sc, SAT_VALUE_UNKNOWN),
+  d_engineState(0)
 {
-  const Options* options = Options::current();
   Trace("decision") << "Creating decision engine" << std::endl;
+}
+
+void DecisionEngine::init()
+{
+  Assert(d_engineState == 0);
+  d_engineState = 1;
 
+  const Options* options = Options::current();
   if(options->incrementalSolving) return;
 
   if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
@@ -60,6 +67,7 @@ namespace CVC4 {
   }
 }
 
+
 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
 {
   d_enabledStrategies.push_back(ds);