mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-02 07:07:52 +00:00
Code Activity

Fix union problem (might not solve all bugs)

Browse source
This commit is contained in:
CEisenhofer 2026-03-20 12:17:44 +01:00
parent 4f884e7d9a
commit 9aaf103ca0
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/euf/euf_sgraph.cpp
View file

@ -533,10 +533,13 @@ namespace euf {
// if (allowed_range) // if (allowed_range)
// std::cout << "using " << seq::snode_label_html(allowed_range, m) << std::endl; // std::cout << "using " << seq::snode_label_html(allowed_range, m) << std::endl;
// If it is a disjunction just take one of the elements
while (m_seq.re.is_union(elem_expr)) {
elem_expr = to_app(elem_expr)->get_arg(0);
}
// unwrap str.unit to get the character expression // unwrap str.unit to get the character expression
expr* ch = nullptr; expr* ch = nullptr;
std::cout << elem->get_sort()->get_name() << std::endl;
if (m_seq.str.is_unit(elem_expr, ch)) if (m_seq.str.is_unit(elem_expr, ch))
elem_expr = ch; elem_expr = ch;