diff options
Diffstat (limited to 'src/theory/arith/constraint.cpp')
-rw-r--r-- | src/theory/arith/constraint.cpp | 5 |
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; } |