diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-14 17:14:30 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-14 17:14:30 +0000 |
| commit | da66d47ddff4315db54bbcd3b8f46cf1040d5fd0 (patch) | |
| tree | 291b115fdc40320e182bd652319b8b104aa7bac1 /src/smt | |
| parent | ce4ba524301ee3a8a297b2c3050e7d2c5ee58d08 (diff) | |
bug ifx, mv
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
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() && |