From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 15 Aug 2014 23:00:45 +0000 (-0400)
Subject: Update smt_engine.cpp
X-Git-Tag: cvc5-1.0.0~6669
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=18da2141dcddf221f0a40782b02a24766f0ed2c7;p=cvc5.git

Update smt_engine.cpp

Code changed but comment didn't, might as well get rid of it.
---

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