From: Tim King <taking@cs.nyu.edu>
Date: Sat, 16 Jun 2012 17:37:33 +0000 (+0000)
Subject: Fixing if condition for trivial equalities in arithmetic. Also some whitespace issues... 
X-Git-Tag: cvc5-1.0.0~7994
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=adae14a07b1019d092b4d5aa0cf809f9d0eca66d;p=cvc5.git

Fixing if condition for trivial equalities in arithmetic. Also some whitespace issues in smt_engine.cpp.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e86353eea..a55ced622 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -542,7 +542,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
   }
   // Turn on justification heuristic of the decision engine for QF_BV and QF_AUFBV
   if(!Options::current()->decisionModeSetByUser) {
-    Options::DecisionMode decMode = 
+    Options::DecisionMode decMode =
       //QF_BV
       ( !d_logic.isQuantified() &&
         d_logic.isPure(THEORY_BV)
@@ -558,7 +558,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
     Trace("smt") << "setting decision mode to " << decMode << std::endl;
     NodeManager::currentNM()->getOptions()->decisionMode = decMode;
   }
- 
+
 }
 
 void SmtEngine::setInfo(const std::string& key, const SExpr& value)
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index eb0c99abe..e4284286e 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1104,7 +1104,8 @@ Constraint TheoryArith::constraintFromFactQueue(){
     Assert(!isSetup(eq));
     Node reEq = Rewriter::rewrite(eq);
     if(reEq.getKind() == CONST_BOOLEAN){
-      if(reEq.getConst<bool>() != isDistinct){
+      if(reEq.getConst<bool>() == isDistinct){
+        // if is (not true), or false
         Assert((reEq.getConst<bool>() && isDistinct) ||
                (!reEq.getConst<bool>() && !isDistinct));
         d_raiseConflict(assertion);