From aafb704cf8e8fdfff92b0faff31123e5ef5328db Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 9 Apr 2026 14:42:48 +0200 Subject: [PATCH] Bug fix in model extraction --- src/smt/seq/seq_nielsen.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index f5d6e3dca..e366389b4 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -4147,15 +4147,16 @@ nielsen_graph::generate_length_constraints(vector& constraint m_solver.assert_expr(ic.fml); for (auto const& kvp : m_sat_node->char_ranges()) { 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(); cases.reserve(ranges.size()); 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(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)); }