diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-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 << " ["; |