From 18da2141dcddf221f0a40782b02a24766f0ed2c7 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Fri, 15 Aug 2014 19:00:45 -0400 Subject: [PATCH] Update smt_engine.cpp Code changed but comment didn't, might as well get rid of it. --- src/smt/smt_engine.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 105ab9749..20851ac94 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1111,10 +1111,8 @@ void SmtEngine::setDefaults() { if (options::arithRewriteEq()) { d_earlyTheoryPP = false; } - // Turn on justification heuristic of the decision engine for QF_BV and QF_AUFBV - // and also use it in stop-only mode for QF_AUFLIA, QF_LRA and Quantifiers - // BUT use neither in ALL_SUPPORTED mode (since it doesn't yet work well - // with incrementality) + + // Set decision mode based on logic (if not set by user) if(!options::decisionMode.wasSetByUser()) { decision::DecisionMode decMode = // ALL_SUPPORTED -- 2.30.2