- This fixes a problem where simplex produced the same conflict in the single check call.

- This increases the number of substitutions that ppAssert can solve on integer equations.

1 files changed, 3 insertions, 2 deletions

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 3cb5464da..d2a0d9bfa 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -26,7 +26,7 @@ ConstraintType constraintTypeOfComparison(const Comparison& cmp){
       if(l.leadingCoefficientIsPositive()){ // (< x c)
         return UpperBound;
       }else{
-        return LowerBound; // (< (-x) c) 
+        return LowerBound; // (< (-x) c)
       }
     }
   case GT:
@@ -482,7 +482,8 @@ Constraint ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const
     }else{
       pair<SortedConstraintMapIterator, bool> negInsertAttempt;
       negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection()));
-      Assert(negInsertAttempt.second);
+      Assert(negInsertAttempt.second
+             || ! negInsertAttempt.first->second.hasConstraintOfType(negC->getType()));
       negPos = negInsertAttempt.first;
     }