From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 1 Dec 2012 00:31:38 +0000 (+0000)
Subject: definition-expansion fixed for get-model, resolves bug 411
X-Git-Tag: cvc5-1.0.0~7502
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7d9c9678999e24e1c8bfa1080ed4f0fb3fa089a9;p=cvc5.git

definition-expansion fixed for get-model, resolves bug 411
---

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;
   }