2 files changed, 34 insertions, 8 deletions

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 8454ca210..1ebbe49e0 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -745,9 +745,8 @@ bool Comparison::isNormalGEQ() const {
       return false;
     }else{
       if(left.isIntegral()){
-        return left.denominatorLCMIsOne() && left.numeratorGCDIsOne();
+        return left.signNormalizedReducedSum();
       }else{
-        Debug("nf::tmp") << "imme sdfhkdjfh "<< left.leadingCoefficientIsAbsOne() << endl;
         return left.leadingCoefficientIsAbsOne();
       }
     }
@@ -768,7 +767,7 @@ bool Comparison::isNormalLT() const {
       return false;
     }else{
       if(left.isIntegral()){
-        return left.denominatorLCMIsOne() && left.numeratorGCDIsOne();
+        return left.signNormalizedReducedSum();
       }else{
         return left.leadingCoefficientIsAbsOne();
       }
@@ -889,6 +888,7 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){
   Polynomial left = sp.getPolynomial();
   Rational right = - (sp.getConstant().getValue());
 
+
   Monomial m = left.getHead();
   Assert(!m.isConstant());
 
@@ -899,16 +899,31 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){
   Polynomial newLeft = left * mult;
   Rational rightMult = right * mult;
 
+  bool negateResult = false;
+  if(!newLeft.leadingCoefficientIsPositive()){
+    // multiply by -1
+    // a: left >= right or b: left > right
+    // becomes
+    // a: -left <= -right or b: -left < -right
+    // a: not (-left > -right) or b: (not -left >= -right)
+    newLeft = -newLeft;
+    rightMult = -rightMult;
+    k = (kind::GT == k) ? kind::GEQ : kind::GT;
+    negateResult = true;
+    // the later stages handle:
+    // a: not (-left >= -right + 1) or b: (not -left >= -right)
+  }
 
+  Node result = Node::null();
   if(rightMult.isIntegral()){
     if(k == kind::GT){
       // (> p z)
       // (>= p (+ z 1))
       Constant rightMultPlusOne = Constant::mkConstant(rightMult + 1);
-      return toNode(kind::GEQ, newLeft, rightMultPlusOne);
+      result = toNode(kind::GEQ, newLeft, rightMultPlusOne);
     }else{
       Constant newRight = Constant::mkConstant(rightMult);
-      return toNode(kind::GEQ, newLeft, newRight);
+      result = toNode(kind::GEQ, newLeft, newRight);
     }
   }else{
     //(>= l (/ n d))
@@ -916,7 +931,13 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){
     //This also hold for GT as (ceil (/ n d)) > (/ n d)
     Integer ceilr = rightMult.ceiling();
     Constant ceilRight = Constant::mkConstant(ceilr);
-    return toNode(kind::GEQ, newLeft, ceilRight);
+    result = toNode(kind::GEQ, newLeft, ceilRight);
+  }
+  Assert(!result.isNull());
+  if(negateResult){
+    return result.notNode();
+  }else{
+    return result;
   }
 }
 
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index bcf9cbfa4..c6af7010f 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -76,12 +76,13 @@ namespace arith {
  *     (exists realMonomial (monomialList qpolynomial))
  *     abs(monomialCoefficient (head (monomialList qpolynomial))) == 1
  *
- * integer_cmp := (<= zpolynomial constant)
+ * integer_cmp := (>= zpolynomial constant)
  *   where
  *     not (exists constantMonomial (monomialList zpolynomial))
  *     (forall integerMonomial (monomialList zpolynomial))
  *     the gcd of all numerators of coefficients is 1
  *     the denominator of all coefficients and the constant is 1
+ *     the leading coefficient is positive
  *
  * rational_eq := (= qvarlist qpolynomial)
  *   where
@@ -939,6 +940,10 @@ public:
   bool denominatorLCMIsOne() const;
   bool numeratorGCDIsOne() const;
 
+  bool signNormalizedReducedSum() const {
+    return leadingCoefficientIsPositive() && denominatorLCMIsOne() && numeratorGCDIsOne();
+  }
+
   /**
    * Returns the Least Common Multiple of the denominators of the coefficients
    * of the monomials.
@@ -1265,7 +1270,7 @@ private:
    * Creates a comparison equivalent to (k l 0).
    * k is either GT or GEQ.
    * It is not the case that all variables in l are integral.
-   */  
+   */
   static Node mkRatInequality(Kind k, const Polynomial& l);
 
 public: