diff options
-rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0f755aa01..fb8b78759 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1219,6 +1219,15 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF Kind k = n.getKind(); if(k != kind::APPLY && n.getNumChildren() == 0) { + SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n); + if(i != d_smt.d_definedFunctions->end()) { + // replacement must be closed + if((*i).second.getFormals().size() > 0) { + throw TypeCheckingException(n.toExpr(), std::string("Defined function requires arguments: `") + n.toString() + "'"); + } + // don't bother putting in the cache + return (*i).second.getFormula(); + } // don't bother putting in the cache return n; } |