From: Tim King <taking@cs.nyu.edu>
Date: Fri, 11 May 2012 01:29:11 +0000 (+0000)
Subject: Partially fixes something-like-a-problem with TheoryArith::getDeltaValue().
X-Git-Tag: cvc5-1.0.0~8190
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5181426cd8def23d67b69227fff033ef12850e68;p=cvc5.git

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 6bb3821da..1179de685 100644
--- 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();
+      }
+    }
   }
 }