diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-18 12:17:00 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-18 12:17:00 +0200 |
| commit | 1856daa190f0b5ca5662408d33f3f70d069b27f7 (patch) | |
| tree | cb3c7ed658fcdfe9fae49da95be6e9f8433c0719 | |
| parent | efe80a0aa2fba812264c332d0ab729d935ea1fa1 (diff) | |
Fix for no condense func values.
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
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; } |