Fix bug in hasBoundVar (#5600)

Led to issues while debugging another issue related to free variables in assumptions.

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 9d1c6ab41c4b7bec1181a068620cb5c87109efad..f41bef37b8ae8f1662312d824d952ad0a3b6e399 100644 (file)
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -261,7 +261,11 @@ bool hasBoundVar(TNode n)
     {
       for (auto i = n.begin(); i != n.end() && !hasBv; ++i)
       {
-        hasBv = hasBoundVar(*i);
+        if (hasBoundVar(*i))
+        {
+          hasBv = true;
+          break;
+        }
       }
     }
     if (!hasBv && n.hasOperator())