mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

merge comment

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-16 13:39:17 +02:00
parent 0371bbd192
commit 9e79fe0a51
1 changed files with 4 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/finite_set_decl_plugin.cpp
View file

@ -222,8 +222,6 @@ bool finite_set_decl_plugin::is_value(app * e) const {
if (a->get_num_args() != 1) if (a->get_num_args() != 1)
return false; return false;
expr* elem = a->get_arg(0); expr* elem = a->get_arg(0);
if (!is_app(elem))
return false;
if (!m_manager->is_value(elem)) if (!m_manager->is_value(elem))
return false; return false;
continue; continue;
@ -232,11 +230,12 @@ bool finite_set_decl_plugin::is_value(app * e) const {
// Check if it's a union // Check if it's a union
if (is_app_of(a, m_family_id, OP_FINITE_SET_UNION)) { if (is_app_of(a, m_family_id, OP_FINITE_SET_UNION)) {
// Add arguments to todo list // Add arguments to todo list
for (unsigned i = 0; i < a->get_num_args(); ++i) { for (auto arg : *a)
todo.push_back(a->get_arg(i)); todo.push_back(arg);
}
continue; continue;
} }
// can add also ranges where lo and hi are values.
// If it's none of the above, it's not a value // If it's none of the above, it's not a value
return false; return false;