From e62ba9b60b2d8030a999644cab6bc49798c9f269 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 6 May 2026 15:46:53 +0200 Subject: [PATCH] stoi lemmas might have been forgotten so we need to reassert --- src/smt/theory_nseq.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index cab52156d..36833ec0a 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -1594,11 +1594,15 @@ namespace smt { ctx.mk_th_axiom(get_id(), 3, clause); } - m_stoi_depth.insert_if_not_there(stoi_e, 0); - m_stoi_depth[stoi_e] = k; + if (m_stoi_depth.contains(stoi_e)) { + unsigned prev = m_stoi_depth[stoi_e]; + ctx.push_trail(remove_obj_map(m_stoi_depth, stoi_e, prev)); + m_stoi_depth.remove(stoi_e); + } + ctx.push_trail(insert_obj_map(m_stoi_depth, stoi_e)); + m_stoi_depth.insert(stoi_e, k); progress = true; } - return !progress; }