Fix to bug449. Adds shared constants to the set of DeltaRationals that must be in the final total order.

1 files changed, 12 insertions, 0 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1d89c02d4..74e0ad296 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -674,6 +674,10 @@ bool TheoryArith::AssertDisequality(Constraint constraint){
 
 void TheoryArith::addSharedTerm(TNode n){
   Debug("arith::addSharedTerm") << "addSharedTerm: " << n << endl;
+  if(n.isConst()){
+    d_partialModel.invalidateDelta();
+  }
+
   d_congruenceManager.addSharedTerm(n);
   if(!n.isConst() && !isSetup(n)){
     Polynomial poly = Polynomial::parsePolynomial(n);
@@ -2102,6 +2106,14 @@ Rational TheoryArith::deltaValueForTotalOrder() const{
     relevantDeltaValues.insert(rhsValue);
   }
 
+  for(shared_terms_iterator shared_iter = shared_terms_begin(),
+        shared_end = shared_terms_end(); shared_iter != shared_end; ++shared_iter){
+    Node sharedCurr = *shared_iter;
+    if(sharedCurr.getKind() == CONST_RATIONAL){
+      relevantDeltaValues.insert(sharedCurr.getConst<Rational>());:
+    }
+  }
+
   for(ArithVar v = 0; v < d_variables.size(); ++v){
     const DeltaRational& value = d_partialModel.getAssignment(v);
     relevantDeltaValues.insert(value);