1 files changed, 19 insertions, 26 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f360ae2fd..b2f7d6ccc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2277,8 +2277,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
     if(!childrenPushed) {
       Kind k = n.getKind();
 
-      // Apart from apply, we can short circuit leaves
-      if(k != kind::APPLY && n.getNumChildren() == 0) {
+      // we can short circuit (variable) leaves
+      if(n.isVar()) {
         SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n);
         if(i != d_smt.d_definedFunctions->end()) {
           // replacement must be closed
@@ -2372,15 +2372,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
         node = t->expandDefinition(req, n);
       }
 
-      // there should be children here, otherwise we short-circuited a result-push/continue, above
-      if (node.getNumChildren() == 0) {
-        Debug("expand") << "Unexpectedly no children..." << node << endl;
-      }
-      // This invariant holds at the moment but it is concievable that a new theory
-      // might introduce a kind which can have children before definition expansion but doesn't
-      // afterwards.  If this happens, remove this assertion.
-      Assert(node.getNumChildren() > 0);
-
       // the partial functions can fall through, in which case we still
       // consider their children
       worklist.push(make_triple(Node(n), node, true));            // Original and rewritten result
@@ -2394,22 +2385,24 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
       // Reconstruct the node from it's (now rewritten) children on the stack
 
       Debug("expand") << "cons : " << node << endl;
-      //cout << "cons : " << node << endl;
-      NodeBuilder<> nb(node.getKind());
-      if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        Debug("expand") << "op   : " << node.getOperator() << endl;
-        //cout << "op   : " << node.getOperator() << endl;
-        nb << node.getOperator();
-      }
-      for(size_t i = 0; i < node.getNumChildren(); ++i) {
-        Assert(!result.empty());
-        Node expanded = result.top();
-        result.pop();
-        //cout << "exchld : " << expanded << endl;
-        Debug("expand") << "exchld : " << expanded << endl;
-        nb << expanded;
+      if(node.getNumChildren()>0) {
+        //cout << "cons : " << node << endl;
+        NodeBuilder<> nb(node.getKind());
+        if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+          Debug("expand") << "op   : " << node.getOperator() << endl;
+          //cout << "op   : " << node.getOperator() << endl;
+          nb << node.getOperator();
+        }
+        for(size_t i = 0; i < node.getNumChildren(); ++i) {
+          Assert(!result.empty());
+          Node expanded = result.top();
+          result.pop();
+          //cout << "exchld : " << expanded << endl;
+          Debug("expand") << "exchld : " << expanded << endl;
+          nb << expanded;
+        }
+        node = nb;
       }
-      node = nb;
       cache[n] = n == node ? Node::null() : node;           // Only cache once all subterms are expanded
       result.push(node);
     }