From af2082a1aa5fe62c6ebaa69dc9095e66deba8587 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Oct 2025 14:52:53 +0200 Subject: [PATCH] add a comment, remove } Signed-off-by: Nikolaj Bjorner --- src/model/finite_set_value_factory.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp index 9fee35d9e..54b7555f0 100644 --- a/src/model/finite_set_value_factory.cpp +++ b/src/model/finite_set_value_factory.cpp @@ -27,6 +27,9 @@ expr * finite_set_value_factory::get_some_value(sort * s) { return u.mk_empty(s); } +/** + * create sets {}, {a}, {b}, {a,b}, {c}, {a,c}, {b,c}, {a,b,c}, {d}, ... + */ expr * finite_set_value_factory::get_fresh_value(sort * s) { sort* elem_sort = nullptr; VERIFY(u.is_finite_set(s, elem_sort)); @@ -50,7 +53,6 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) { auto e = m_model.get_fresh_value(elem_sort); if (!e) return nullptr; - register_value(e); auto r = u.mk_singleton(e); register_value(r); return r; @@ -59,9 +61,8 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) { // Case 3: Find greatest power of 2 N < values.size() and create union // Find the greatest N that is a power of 2 and N < values.size() unsigned N = 1; - while (N * 2 < values.size()) { - N *= 2; - } + while (N * 2 < values.size()) + N *= 2; auto r = u.mk_union(values.get(values.size() - N), values.get(N)); register_value(r);