From 7f604fe97bd85efbe6ffcf17140905cdb34c7468 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 7 Mar 2014 23:47:56 -0500 Subject: [PATCH] Fix bug 554 (nominally). --- src/smt/smt_engine.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 02542b640..1bbc99f09 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3677,8 +3677,15 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin // Expand, then normalize hash_map cache; n = d_private->expandDefinitions(n, cache); - n = d_private->rewriteBooleanTerms(n); - n = Rewriter::rewrite(n); + // There are two ways model values for terms are computed (for historical + // reasons). One way is that used in check-model; the other is that + // used by the Model classes. It's not clear to me exactly how these + // two are different, but they need to be unified. This ugly hack here + // is to fix bug 554 until we can revamp boolean-terms and models [MGD] + if(!n.getType().isFunction()) { + n = d_private->rewriteBooleanTerms(n); + n = Rewriter::rewrite(n); + } Trace("smt") << "--- getting value of " << n << endl; TheoryModel* m = d_theoryEngine->getModel(); -- 2.30.2