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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e86353eea7319f3d9ae0e2bb7f52e2b97063bb1e..a55ced6227beea0f1d251f19161b0f1e8f551a0f 100644 (file)
--- 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 eb0c99abe4d481be4d312585acf33b59776cf349..e4284286e8254c2a2541ede62281d136557a4013 100644 (file)
--- 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);