diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-14 20:57:12 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-14 20:57:12 +0000 |
commit | 5b5a421d79d12a31edde3902f2b8ddec6a3ca684 (patch) | |
tree | 738662afe397657be3e793a4f38a9cf0e13f4cd7 /src/theory/arith | |
parent | 7d298cf9abe3cb09c897eafe6fab5ef636be4c27 (diff) |
fixes for shared term registration. previously the type was not considered when looking at theories of the term and for a term like
read(a, f(x))
the term f(x) would not be registered to arithmetic in AUFLIA. this fixies the issue of bug 330 and moves it to some other assertion fail.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1179de685..d660cb4cd 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1487,11 +1487,10 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { default: { if(isSetup(n)){ - ArithVar var = d_arithvarNodeMap.asArithVar(n); - return d_partialModel.getAssignment(var); + ArithVar var = d_arithvarNodeMap.asArithVar(n); + return d_partialModel.getAssignment(var); }else{ - Warning() << "you did not setup this up!: " << n << endl; - return DeltaRational(); + Unreachable(); } } } |