From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 8 Mar 2014 04:47:56 +0000 (-0500)
Subject: Fix bug 554 (nominally).
X-Git-Tag: cvc5-1.0.0~7038
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f604fe97bd85efbe6ffcf17140905cdb34c7468;p=cvc5.git

Fix bug 554 (nominally).
---

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<Node, Node, NodeHashFunction> 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();