From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 14 Jun 2012 17:14:30 +0000 (+0000)
Subject: bug ifx, mv
X-Git-Tag: cvc5-1.0.0~8017
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=da66d47ddff4315db54bbcd3b8f46cf1040d5fd0;p=cvc5.git

bug ifx, mv
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 747c92c0c..75d306663 100644
--- 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() &&