3 files changed, 26 insertions, 4 deletions
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 12110fab4..ed256faa1 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -93,6 +93,10 @@ public:
     return *(this) + (a * negOne);
   }
 
+  DeltaRational operator-() const{
+    return DeltaRational(-c, -k);
+  }
+
   DeltaRational operator/(const Rational& a) const{
     CVC4::Rational tmpC = c/a;
     CVC4::Rational tmpK = k/a;
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 986df5f80..c90be63b9 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -532,10 +532,26 @@ DeltaRational Comparison::normalizedDeltaRational() const {
   case kind::EQUAL:
   case kind::DISTINCT:
     {
-      Monomial firstRight = getRight().getHead();
+      Polynomial right = getRight();
+      Monomial firstRight = right.getHead();
       if(firstRight.isConstant()){
-        return DeltaRational(firstRight.getConstant().getValue(), 0);
-      }else{
+        DeltaRational c = DeltaRational(firstRight.getConstant().getValue(), 0);
+        Polynomial left = getLeft();
+        if(!left.allIntegralVariables()){
+          return c;
+          //this is a qpolynomial and the sign of the leading
+          //coefficient will not change after the diff below
+        } else{
+          // the polynomial may be a z polynomial in which case
+          // taking the diff is the simplest and obviously correct means
+          Polynomial diff = right.singleton() ? left : left - right.getTail();
+          if(diff.leadingCoefficientIsPositive()){
+            return c;
+          }else{
+            return -c;
+          }
+        }
+      }else{ // The constant is 0 sign cannot change
         return DeltaRational(0, 0);
       }
     }
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index b5475586a..8fb99a9ae 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -493,7 +493,9 @@ Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar
     const Rational& coeff = entry.getCoefficient();
     bool weakening = false;
     Constraint c = weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar);
-    Debug("weak") << "weak : " << weakening << " " << c->assertedToTheTheory()
+    Debug("weak") << "weak : " << weakening << " "
+                  << c->assertedToTheTheory() << " "
+                  << d_partialModel.getAssignment(v) << " "
                   << c << endl
                   << c->explainForConflict() << endl;
     anyWeakenings = anyWeakenings || weakening;