Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.

1 files changed, 1 insertions, 1 deletions

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 77e7e1060..27fb0bb02 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -339,7 +339,7 @@ bool SimplexDecisionProcedure::propagateCandidateBound(ArithVar basic, bool uppe
           explainNonbasicsLowerBound(basic, nb);
         }
         Node explanation = nb;
-        d_propManager.propagate(bestImplied, explanation);
+        d_propManager.propagate(bestImplied, explanation, false);
         return true;
       }else{
         Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl;