bug ifx, mv

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 747c92c0ce58f598229e977e8f3ee8333665c562..75d306663fcf7c6bf019d64b77444e3d76c6ff9b 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -329,10 +329,13 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
 
 void SmtEngine::finishInit() {
   d_decisionEngine = new DecisionEngine(d_context, d_userContext);
+  d_decisionEngine->init();   // enable appropriate strategies
+
   d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
+
   d_theoryEngine->setPropEngine(d_propEngine);
   d_theoryEngine->setDecisionEngine(d_decisionEngine);
-  // d_decisionEngine->setPropEngine(d_propEngine);
+
 }
 
 void SmtEngine::finalOptionsAreSet() {
@@ -350,8 +353,6 @@ void SmtEngine::finalOptionsAreSet() {
   d_fullyInited = true;
   d_logic.lock();
 
-  d_decisionEngine->init();
-
   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(true));
   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(false).notNode());
 }
@@ -532,7 +533,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
     d_earlyTheoryPP = false;
   }
   // Turn on justification heuristic of the decision engine for QF_BV and QF_AUFBV
-  if(! Options::current()->repeatSimpSetByUser) {
+  if(!Options::current()->decisionModeSetByUser) {
     Options::DecisionMode decMode = 
       //QF_BV
       ( !d_logic.isQuantified() &&