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, 9 insertions, 0 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 11f3bdcb9..ae9caf0eb 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -197,10 +197,19 @@ class CVC4_PUBLIC SmtEngine {
    * as often as you like.  Should be called whenever the final options
    * and logic for the problem are set (at least, those options that are
    * not permitted to change after assertions and queries are made).
+   *
+   * FIXME: Above comment not true. Please don't call this more than
+   * once. (6/14/2012 -- K)
    */
   void finalOptionsAreSet();
 
   /**
+   * Create theory engine, prop engine, decision engine. Called by
+   * finalOptionsAreSet()
+   */
+  void finishInit();
+
+  /**
    * This is called by the destructor, just before destroying the
    * PropEngine, TheoryEngine, and DecisionEngine (in that order).  It
    * is important because there are destruction ordering issues