From e0ee22291dff96679a98ac77f3fbaa01de3ab035 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 27 Jul 2018 02:03:56 -0500
Subject: [PATCH] Fix Node::hasFreeVar for function variables (#2216)

A Node has free variables if its operator has free variables.
---
 src/expr/node.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 0503c7932..fdb1e4d90 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -181,6 +181,10 @@ bool NodeTemplate<ref_count>::hasFreeVar()
       }
       // must visit quantifiers again to clean up below
       visited[cur] = !isQuant;
+      if (cur.hasOperator())
+      {
+        visit.push_back(cur.getOperator());
+      }
       for (const TNode& cn : cur)
       {
         visit.push_back(cn);
-- 
2.30.2