From 9aaf103ca04b10f7c2c0f4621166522ae21dff40 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 20 Mar 2026 12:17:44 +0100 Subject: [PATCH] Fix union problem (might not solve all bugs) --- src/ast/euf/euf_sgraph.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp index 34429396e..25e6de2d5 100644 --- a/src/ast/euf/euf_sgraph.cpp +++ b/src/ast/euf/euf_sgraph.cpp @@ -533,10 +533,13 @@ namespace euf { // if (allowed_range) // 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 expr* ch = nullptr; - std::cout << elem->get_sort()->get_name() << std::endl; if (m_seq.str.is_unit(elem_expr, ch)) elem_expr = ch;