From e314cee5558babad33e5c8228c74701abc0106cc Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 19 Jul 2013 11:13:40 -0400
Subject: [PATCH] Minor fix for --no-condense-function-values

---
 src/theory/model.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

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;
 }
 
-- 
2.30.2