From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 20 Feb 2013 23:11:54 +0000 (-0500)
Subject: Fix for SmtEngine::expandDefinitions()---improper TypeCheckingException
X-Git-Tag: cvc5-1.0.0~7376^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=118e998b926870e817cd57c49b91fdb27948e828;p=cvc5.git

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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2a73cb444..5a4c1ca58 100644
--- 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();