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

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 234b137c8adbc0e564a16c45b64076984232aaaf..840c8bc3ac7ce929e42b5026a6763624c0d1bee2 100644 (file)
--- 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;
 }