From 7fc68d20ea5b983a27c8c2cd035b25525a9cd507 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Apr 2026 19:16:18 -0700 Subject: [PATCH] brain got parked somewhere? Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index ac4c34fa3..5ea1b1cd5 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -3965,8 +3965,8 @@ namespace seq { void nielsen_graph::dec_edge_mod_counts(nielsen_edge* e) { auto& sub = e->subst(); - for (unsigned i = sub.size(); i > 0; i++) { - unsigned id = sub[i - 1].m_var->id(); + for (unsigned i = sub.size(); i-- > 0;) { + unsigned id = sub[i].m_var->id(); unsigned prev = m_length_backtrack.back(); m_length_backtrack.pop_back(); m_length_term.pop_back(); @@ -3975,7 +3975,7 @@ namespace seq { else m_length_info.insert(id, prev); - id = sub[i - 1].m_var->id(); + id = sub[i].m_var->id(); prev = 0; VERIFY(m_mod_cnt.find(id, prev)); SASSERT(prev >= 1);