From 68c393b714e3d344df28f44fb1590ad1a73ba819 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 4 Dec 2014 01:39:53 -0500
Subject: [PATCH] Fix segfault in lambdas when constructed via API.

---
 src/smt/smt_engine.cpp | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8f5ba2024..659051725 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1714,11 +1714,13 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
       }
 
       // otherwise expand it
-      if (k == kind::APPLY) {
+      if (k == kind::APPLY && n.getOperator().getKind() != kind::LAMBDA) {
         // application of a user-defined symbol
         TNode func = n.getOperator();
-        SmtEngine::DefinedFunctionMap::const_iterator i =
-          d_smt.d_definedFunctions->find(func);
+        SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(func);
+        if(i == d_smt.d_definedFunctions->end()) {
+          throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'");
+        }
         DefinedFunction def = (*i).second;
         vector<Node> formals = def.getFormals();
 
@@ -1728,9 +1730,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
           string name = func.getAttribute(expr::VarNameAttr());
           Debug("expand") << "     : \"" << name << "\"" << endl;
         }
-        if(i == d_smt.d_definedFunctions->end()) {
-          throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'");
-        }
         if(Debug.isOn("expand")) {
           Debug("expand") << " defn: " << def.getFunction() << endl
                           << "       [";
-- 
2.30.2