Fix for no condense func values.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a1eca35fa210e032379be7ac26e9dbb86e929c1a..f203c7d1e6152fc72e4e05e660793fbf2a7d67df 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3841,8 +3841,10 @@ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
   Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl;
   Node realValue = mpost.rewriteAs(value, expectedType);
   Debug("boolean-terms") << "postproc: realval " << realValue << " expect type " << expectedType << endl;
-  realValue = Rewriter::rewrite(realValue);
-  Debug("boolean-terms") << "postproc: after rewrite " << realValue << endl;
+  if(options::condenseFunctionValues()) {
+    realValue = Rewriter::rewrite(realValue);
+    Debug("boolean-terms") << "postproc: after rewrite " << realValue << endl;
+  }
   return realValue;
 }