Fix Node::hasFreeVar for function variables (#2216)

A Node has free variables if its operator has free variables.

1 files changed, 4 insertions, 0 deletions

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