Making propagation more conversative.

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){