mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-30 23:53:44 +00:00
Code Activity

Bug

Browse source
This commit is contained in:
CEisenhofer 2026-03-20 12:11:18 +01:00
parent a873d5cdda
commit 4f884e7d9a
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -527,8 +527,8 @@ namespace euf {
snode* sgraph::brzozowski_deriv(snode* re, snode* elem, snode* allowed_range) { snode* sgraph::brzozowski_deriv(snode* re, snode* elem, snode* allowed_range) {
expr* re_expr = re->get_expr(); expr* re_expr = re->get_expr();
expr* elem_expr = elem->get_expr(); expr* elem_expr = elem->get_expr();
if (!re_expr || !elem_expr) SASSERT(re_expr);
return nullptr; SASSERT(elem_expr);
// std::cout << "Derivative of " << seq::snode_label_html(re, m) << "\nwith respect to " << seq::snode_label_html(elem, m) << std::endl; // std::cout << "Derivative of " << seq::snode_label_html(re, m) << "\nwith respect to " << seq::snode_label_html(elem, m) << std::endl;
// 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;
@ -536,6 +536,7 @@ namespace euf {
// 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;
@ -579,8 +580,10 @@ namespace euf {
else else
elem_expr = lo; elem_expr = lo;
} }
std::cout << "Unexpected node: " << mk_pp(elem_expr, m) << std::endl; else {
UNREACHABLE(); std::cout << "Unexpected node: " << mk_pp(elem_expr, m) << std::endl;
UNREACHABLE();
}
} }
} }