diff options
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 5b40e03bc..c71f2a6bd 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2662,7 +2662,16 @@ bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{ ConstraintType t = ub ? UpperBound : LowerBound; const DeltaRational& a = d_partialModel.getAssignment(v); - return NullConstraint != d_constraintDatabase.getBestImpliedBound(v, t, a); + Constraint strongestPossible = d_constraintDatabase.getBestImpliedBound(v, t, a); + if(strongestPossible == NullConstraint){ + return false; + }else{ + bool assertedToTheTheory = strongestPossible->assertedToTheTheory(); + bool canBePropagated = strongestPossible->canBePropagated(); + bool hasProof = strongestPossible->hasProof(); + + return !assertedToTheTheory && canBePropagated && !hasProof; + } }else{ return false; } @@ -2800,6 +2809,10 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){ ++instance; cout << "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl; + if(rowLength >= options::arithPropagateMaxLength()){ + return false; + } + if(hasCount.lowerBoundCount() == rowLength){ success |= attemptFull(ridx, false); }else if(hasCount.lowerBoundCount() + 1 == rowLength){ |