diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 14 |
1 files 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(); + } + } } } |