From 5b5a421d79d12a31edde3902f2b8ddec6a3ca684 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Mon, 14 May 2012 20:57:12 +0000 Subject: 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. --- src/theory/arith/theory_arith.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'src/theory/arith') 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(); } } } -- cgit v1.2.3