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

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

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 0503c79326ca15096656a3bdecbc4d7c1013ab50..fdb1e4d9001cd03ac3da41551f095da4234c048c 100644 (file)
--- 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);