Partially fixes something-like-a-problem with TheoryArith::getDeltaValue().

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6bb3821da97c90926e61ff848fe5535ba6099e5a..1179de685e37da4c515192a0a8b724fc9e155cb7 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -476,6 +476,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){
 }
 
 void TheoryArith::addSharedTerm(TNode n){
+  Debug("arith::addSharedTerm") << "addSharedTerm: " << n << endl;
   d_congruenceManager.addSharedTerm(n);
   if(!n.isConst() && !isSetup(n)){
     Polynomial poly = Polynomial::parsePolynomial(n);
@@ -1484,10 +1485,15 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
 
 
   default:
-  {
-    ArithVar var = d_arithvarNodeMap.asArithVar(n);
-    return d_partialModel.getAssignment(var);
-  }
+    {
+      if(isSetup(n)){
+       ArithVar var = d_arithvarNodeMap.asArithVar(n);
+       return d_partialModel.getAssignment(var);
+      }else{
+       Warning() << "you did not setup this up!: " << n << endl;
+       return DeltaRational();
+      }
+    }
   }
 }