From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 19 Jul 2013 15:13:40 +0000 (-0400)
Subject: Minor fix for --no-condense-function-values
X-Git-Tag: cvc5-1.0.0~7287^2~56
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e314cee5558babad33e5c8228c74701abc0106cc;p=cvc5.git

Minor fix for --no-condense-function-values
---

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 234b137c8..840c8bc3a 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -53,8 +53,10 @@ Node TheoryModel::getValue(TNode n) const {
   Node nn = d_substitutions.apply(n);
   //get value in model
   nn = getModelValue(nn);
-  //normalize
-  nn = Rewriter::rewrite(nn);
+  if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
+    //normalize
+    nn = Rewriter::rewrite(nn);
+  }
   return nn;
 }