diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-12-04 01:39:53 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-12-04 01:39:53 -0500 |
commit | 68c393b714e3d344df28f44fb1590ad1a73ba819 (patch) | |
tree | 675fddfcb9c34d47a083d75a64f9b5d3f2a97c53 /src/smt | |
parent | 9571f1f605f4465ffe049d7df22bc1dbabd50657 (diff) |
Fix segfault in lambdas when constructed via API.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 11 |
1 files 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 << " ["; |