From 7d9c9678999e24e1c8bfa1080ed4f0fb3fa089a9 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 1 Dec 2012 00:31:38 +0000
Subject: [PATCH] definition-expansion fixed for get-model, resolves bug 411

---
 src/smt/smt_engine.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

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