diff options
author | Tim King <taking@cs.nyu.edu> | 2011-11-29 21:11:45 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-11-29 21:11:45 +0000 |
commit | e9198d9b99c6037165362870436b45826674303f (patch) | |
tree | b5e8d01a53d38d353dae7c16351ff9206e1f96c6 /src/theory/arith/simplex.cpp | |
parent | 8b202bab8442c927e9ac18a35c71a82444acf63b (diff) |
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.
Diffstat (limited to 'src/theory/arith/simplex.cpp')
-rw-r--r-- | src/theory/arith/simplex.cpp | 2 |
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; |