From 9e79fe0a51b90001dcdd883cab21068c2ca8f125 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Oct 2025 13:39:17 +0200 Subject: [PATCH] merge comment Signed-off-by: Nikolaj Bjorner --- src/ast/finite_set_decl_plugin.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 891d5f6b9..028231fba 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -222,8 +222,6 @@ bool finite_set_decl_plugin::is_value(app * e) const { if (a->get_num_args() != 1) return false; expr* elem = a->get_arg(0); - if (!is_app(elem)) - return false; if (!m_manager->is_value(elem)) return false; continue; @@ -232,11 +230,12 @@ bool finite_set_decl_plugin::is_value(app * e) const { // Check if it's a union if (is_app_of(a, m_family_id, OP_FINITE_SET_UNION)) { // Add arguments to todo list - for (unsigned i = 0; i < a->get_num_args(); ++i) { - todo.push_back(a->get_arg(i)); - } + for (auto arg : *a) + todo.push_back(arg); continue; } + + // can add also ranges where lo and hi are values. // If it's none of the above, it's not a value return false;