mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

Deriving by allchar should not crash

Browse source
This commit is contained in:
CEisenhofer 2026-04-09 11:48:35 +02:00
parent 8eb0ac29d9
commit 38d725dc5a
2 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -559,9 +559,10 @@ namespace euf {
if (ele_sort != elem_expr->get_sort()) {
// std::cout << "Different sorts: " << ele_sort->get_name() << " vs " << elem_expr->get_sort()->get_name() << std::endl;
expr* lo = nullptr, *hi = nullptr;
if (m_seq.re.is_full_char(elem_expr))
return nullptr;
if (m_seq.re.is_range(elem_expr, lo, hi) && lo) {
if (m_seq.re.is_full_char(elem_expr)) {
elem_expr = m_seq.str.mk_char(0);
}
else if (m_seq.re.is_range(elem_expr, lo, hi) && lo) {
expr* lo_ch = nullptr;
zstring zs;
if (m_seq.str.is_unit(lo, lo_ch))
@ -579,8 +580,7 @@ namespace euf {
}
expr_ref result = m_rewriter.mk_derivative(elem_expr, re_expr);
if (!result)
return nullptr;
SASSERT(result);
return mk(result);
}

6
src/smt/theory_nseq.cpp
View file

@ -687,6 +687,7 @@ namespace smt {
v.reset();
}
};
std::cout << "Nielsen assumptions:\n";
ctx.push_trail(reset_vector(m_nielsen_literals));
for (auto const& c : m_nielsen.sat_node()->constraints()) {
bool was_internalized = ctx.e_internalized(c.fml);
@ -696,6 +697,7 @@ namespace smt {
case l_true:
break;
case l_undef:
//std::cout << "Undef: " << mk_pp(c.fml, m) << "\n";
has_undef = true;
ctx.force_phase(lit);
IF_VERBOSE(2, verbose_stream() <<
@ -708,10 +710,12 @@ namespace smt {
<< "nseq final_check: nielsen assumption " << c.fml << " is false\n";);
ctx.force_phase(lit);
has_undef = true;
ctx.force_phase(lit);
ctx.force_phase(lit);
//std::cout << "False: " << mk_pp(c.fml, m) << "\n";
break;
}
}
std::cout << std::endl;
if (has_undef)
return false;
return true;