- 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, 2 insertions, 14 deletions

diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 964d27464..7efe349e5 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -257,7 +257,7 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
   Assert(d_tableau.isBasic(basic));
   Assert(c->getVariable() == basic);
   Assert(!c->assertedToTheTheory());
-  Assert(c->canBePropagated());
+  //Assert(c->canBePropagated());
   Assert(!c->hasProof());
 
   Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
@@ -279,35 +279,23 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
     if(upperBound){
       if(sgn < 0){
         bound = d_partialModel.getLowerBoundConstraint(nonbasic);
-        //d_partialModel.explainLowerBound(nonbasic, output);
-        //bound = d_partialModel.explainLowerBound(nonbasic);
       }else{
         Assert(sgn > 0);
         bound = d_partialModel.getUpperBoundConstraint(nonbasic);
-        //d_partialModel.explainUpperBound(nonbasic, output);
-        //bound = d_partialModel.explainUpperBound(nonbasic);
       }
     }else{
       if(sgn < 0){
         bound = d_partialModel.getUpperBoundConstraint(nonbasic);
-        //d_partialModel.explainUpperBound(nonbasic, output);
-        //bound =  d_partialModel.explainUpperBound(nonbasic);
       }else{
         Assert(sgn > 0);
         bound = d_partialModel.getLowerBoundConstraint(nonbasic);
-        //d_partialModel.explainLowerBound(nonbasic, output);
-        //bound =  d_partialModel.explainLowerBound(nonbasic);
       }
     }
     Assert(bound != NullConstraint);
     Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl;
     bounds.push_back(bound);
-    //Assert(!bound.isNull());
-    // Debug("arith::explainNonbasics") << "\t" << nonbasic << " " << sgn << " " << bound
-    //                                  << endl;
-    // output << bound;
   }
-  c->propagate(bounds);
+  c->impliedBy(bounds);
   Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
                                    << basic << ") done" << endl;
 }