From f3270fb3629cbc62012ae7eb30843a1bc6d4e3c2 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 25 Nov 2017 14:12:00 -0600
Subject: Fixes for higher-order (#1405)

---
 src/theory/quantifiers/term_util.cpp | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

(limited to 'src/theory/quantifiers/term_util.cpp')

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 4e75f7df8..def9a68bc 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -113,10 +113,19 @@ Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited )
 Node TermUtil::getInstConstAttr( Node n ) {
   if (!n.hasAttribute(InstConstantAttribute()) ){
     Node q;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      q = getInstConstAttr(n[i]);
-      if( !q.isNull() ){
-        break;
+    if (n.hasOperator())
+    {
+      q = getInstConstAttr(n.getOperator());
+    }
+    if (q.isNull())
+    {
+      for (const Node& nc : n)
+      {
+        q = getInstConstAttr(nc);
+        if (!q.isNull())
+        {
+          break;
+        }
       }
     }
     InstConstantAttribute ica;
@@ -277,6 +286,10 @@ void TermUtil::computeVarContains2( Node n, Kind k, std::vector< Node >& varCont
         varContains.push_back( n );
       }
     }else{
+      if (n.hasOperator())
+      {
+        computeVarContains2(n.getOperator(), k, varContains, visited);
+      }
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
         computeVarContains2( n[i], k, varContains, visited );
       }
-- 
cgit v1.2.3