3 files changed, 7 insertions, 4 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 71f41354a..2e6832840 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -520,7 +520,7 @@ public:
 
   /**
    * Create a new, fresh variable for use in a binder expression
-   * (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA).  It is
+   * (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE).  It is
    * an error for this bound variable to exist outside of a binder,
    * and it should also only be used in a single binder expression.
    * That is, two distinct FORALL expressions should use entirely
@@ -539,7 +539,7 @@ public:
 
   /**
    * Create a (nameless) new, fresh variable for use in a binder
-   * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA).
+   * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE).
    * It is an error for this bound variable to exist outside of a
    * binder, and it should also only be used in a single binder
    * expression.  That is, two distinct FORALL expressions should use
diff --git a/src/expr/node.h b/src/expr/node.h
index 5456f3285..cd7a1f839 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -468,6 +468,10 @@ public:
     return getMetaKind() == kind::metakind::NULLARY_OPERATOR;
   }
 
+  /**
+   * Returns true if this node represents a closure, that is an expression
+   * that binds variables.
+   */
   inline bool isClosure() const {
     assertTNodeNotExpired();
     return getKind() == kind::LAMBDA || getKind() == kind::FORALL
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 4e62bc9ad..25ffb0778 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -182,8 +182,7 @@ bool getFreeVariables(TNode n,
       continue;
     }
     Kind k = cur.getKind();
-    bool isQuant = k == kind::FORALL || k == kind::EXISTS || k == kind::LAMBDA
-                   || k == kind::CHOICE;
+    bool isQuant = cur.isClosure();
     std::unordered_map<TNode, bool, TNodeHashFunction>::iterator itv =
         visited.find(cur);
     if (itv == visited.end())