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, 19 insertions, 12 deletions

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index e19307170..6b878ecd0 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -56,10 +56,13 @@ class DecisionEngine {
 
   // Disable creating decision engine without required parameters
   DecisionEngine() : d_result(NULL) {}
+
+  // init/shutdown state
+  unsigned d_engineState;    // 0=pre-init; 1=init,pre-shutdown; 2=shutdown
 public:
   // Necessary functions
 
-  /** Constructor, enables decision stragies based on options */
+  /** Constructor */
   DecisionEngine(context::Context *sc, context::Context *uc);
 
   /** Destructor, currently does nothing */
@@ -90,6 +93,21 @@ public:
     d_cnfStream = cs;
   }
 
+  /* enables decision stragies based on options */
+  void init();
+
+  /**
+   * This is called by SmtEngine, at shutdown time, just before
+   * destruction.  It is important because there are destruction
+   * ordering issues between some parts of the system.  For now,
+   * there's nothing to do here in the DecisionEngine.
+   */
+  void shutdown() {
+    Assert(d_engineState == 1);
+    d_engineState = 2;
+
+    Trace("decision") << "Shutting down decision engine" << std::endl;
+  }
 
   // Interface for External World to use our services
 
@@ -144,17 +162,6 @@ public:
     d_result = val;
   }
 
-  /**
-   * This is called by SmtEngine, at shutdown time, just before
-   * destruction.  It is important because there are destruction
-   * ordering issues between some parts of the system.  For now,
-   * there's nothing to do here in the DecisionEngine.
-   */
-  void shutdown() {
-    Trace("decision") << "Shutting down decision engine" << std::endl;
-  }
-
-
   // External World helping us help the Strategies
 
   /** If one of the enabled strategies needs them  */