From 144b9610867ad4ea021f690f25151e60ab6bce65 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 4 Dec 2020 12:26:12 -0600 Subject: [PATCH] Fix bug in hasBoundVar (#5600) Led to issues while debugging another issue related to free variables in assumptions. --- src/expr/node_algorithm.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 9d1c6ab41..f41bef37b 100644 --- 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()) -- 2.30.2