Fix bug 554 (nominally).

1 files 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<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();