Fix for SmtEngine::expandDefinitions()---improper TypeCheckingException

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2a73cb444007b45fc1b23a627ecf1d4f9d9304d0..5a4c1ca58f615c2d829a94dd426ac05e032c0d00 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1285,7 +1285,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
     if(i != d_smt.d_definedFunctions->end()) {
       // replacement must be closed
       if((*i).second.getFormals().size() > 0) {
-        throw TypeCheckingException(n.toExpr(), string("Defined function requires arguments: `") + n.toString() + "'");
+        //throw TypeCheckingException(n.toExpr(), string("Defined function requires arguments: `") + n.toString() + "'");
       }
       // don't bother putting in the cache
       return (*i).second.getFormula();