Fix to term normalization of integer equalities. Adds a regression test that triggered it.

2 files changed, 12 insertions, 4 deletions

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 5fa6e08c6..986df5f80 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -495,11 +495,14 @@ Polynomial Comparison::normalizedVariablePart() const {
       Polynomial right = getRight();
       if(right.isConstant()){
         return left;
-      }else if(right.containsConstant()){
-        Polynomial noConstant = right.getTail();
-        return left - noConstant;
       }else{
-        return left - right;
+        Polynomial noConstant = right.containsConstant() ? right.getTail() : right;
+        Polynomial diff = left - noConstant;
+        if(diff.leadingCoefficientIsPositive()){
+          return diff;
+        }else{
+          return -diff;
+        }
       }
     }
   default:
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 9ff9ceeb9..be24e43ba 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -207,6 +207,7 @@ Node TheoryArith::AssertLower(Constraint constraint){
   }else if(cmpToUB == 0){
     if(isInteger(x_i)){
       d_constantIntegerVariables.push_back(x_i);
+      Debug("dio::push") << x_i << endl;
     }
     Constraint ub = d_partialModel.getUpperBoundConstraint(x_i);
 
@@ -296,6 +297,7 @@ Node TheoryArith::AssertUpper(Constraint constraint){
   }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i)
     if(isInteger(x_i)){
       d_constantIntegerVariables.push_back(x_i);
+      Debug("dio::push") << x_i << endl;
     }
     Constraint lb = d_partialModel.getLowerBoundConstraint(x_i);
     if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){
@@ -396,6 +398,7 @@ Node TheoryArith::AssertEquality(Constraint constraint){
 
   if(isInteger(x_i)){
     d_constantIntegerVariables.push_back(x_i);
+    Debug("dio::push") << x_i << endl;
   }
 
   // Don't bother to check whether x_i != c_i is in d_diseq
@@ -928,6 +931,7 @@ Node TheoryArith::dioCutting(){
           // If the bounds are equal this is already in the dioSolver
           //Add v = dr as a speculation.
           Comparison eq = mkIntegerEqualityFromAssignment(v);
+          Debug("dio::push") <<v << " " <<  eq.getNode() << endl;
           Assert(!eq.isBoolean());
           d_diosolver.pushInputConstraint(eq, eq.getNode());
           // It does not matter what the explanation of eq is.
@@ -994,6 +998,7 @@ Node TheoryArith::callDioSolver(){
       Assert(orig.getKind() != EQUAL);
       return orig;
     }else{
+      Debug("dio::push") << v << " " << eq.getNode() << endl;
       d_diosolver.pushInputConstraint(eq, orig);
     }
   }