From 5181426cd8def23d67b69227fff033ef12850e68 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 11 May 2012 01:29:11 +0000 Subject: [PATCH] Partially fixes something-like-a-problem with TheoryArith::getDeltaValue(). --- src/theory/arith/theory_arith.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) 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(); + } + } } } -- 2.30.2