From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sun, 18 Oct 2015 10:17:00 +0000 (+0200)
Subject: Fix for no condense func values.
X-Git-Tag: cvc5-1.0.0~6202
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1856daa190f0b5ca5662408d33f3f70d069b27f7;p=cvc5.git

Fix for no condense func values.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a1eca35fa..f203c7d1e 100644
--- 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;
 }