mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-25 05:13:32 +00:00
Code Activity

Bug fix in model extraction

Browse source
This commit is contained in:
CEisenhofer 2026-04-09 14:42:48 +02:00
parent d127055841
commit aafb704cf8
1 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/seq/seq_nielsen.cpp
View file

@ -4147,15 +4147,16 @@ nielsen_graph::generate_length_constraints(vector<length_constraint>& constraint
m_solver.assert_expr(ic.fml); m_solver.assert_expr(ic.fml);
for (auto const& kvp : m_sat_node->char_ranges()) { for (auto const& kvp : m_sat_node->char_ranges()) {
expr_ref_vector cases(m); expr_ref_vector cases(m);
const auto& var = m_sg.nodes()[kvp.m_key]->get_expr(); auto var = m_sg.nodes()[kvp.m_key]->get_expr();
SASSERT(seq().str.is_unit(var));
var = to_app(var)->get_arg(0);
const auto& ranges = kvp.m_value.first.ranges(); const auto& ranges = kvp.m_value.first.ranges();
cases.reserve(ranges.size()); cases.reserve(ranges.size());
for (unsigned i = 0; i < ranges.size(); ++i) { for (unsigned i = 0; i < ranges.size(); ++i) {
cases.push_back(m.mk_and( cases[i] = m.mk_and(
seq().mk_le(seq().mk_char(ranges[i].m_lo), var), seq().mk_le(seq().mk_char(ranges[i].m_lo), var),
seq().mk_le(var, seq().mk_char(ranges[i].m_hi - 1)) seq().mk_le(var, seq().mk_char(ranges[i].m_hi - 1)));
));
} }
m_solver.assert_expr(m.mk_or(cases)); m_solver.assert_expr(m.mk_or(cases));
} }