diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-11 01:29:11 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-11 01:29:11 +0000 |
commit | 5181426cd8def23d67b69227fff033ef12850e68 (patch) | |
tree | cb2c2477e2a814f5fa4c498dbab7aaae576e0803 /src/theory/arith/theory_arith.cpp | |
parent | 021d68c157ee698e706096fc9f4a112f17cd0128 (diff) |
Partially fixes something-like-a-problem with TheoryArith::getDeltaValue().
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-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(); + } + } } } |