From d99f0ce230a9e0a4b6ba8c39cbd5e09c1677a303 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 May 2026 10:30:00 -0700 Subject: [PATCH] use shrink instead of pop in a loop --- src/smt/nseq_context_solver.h | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h index 06dd33fee..853b04d51 100644 --- a/src/smt/nseq_context_solver.h +++ b/src/smt/nseq_context_solver.h @@ -125,11 +125,9 @@ namespace smt { void pop(unsigned n) override { SASSERT(n <= m_frame_bounds.size()); unsigned target = m_frame_bounds[m_frame_bounds.size() - n]; - m_deps.pop_back(); - } - for (unsigned i = 0; i < n; i++) { - m_frame_bounds.pop_back(); - } + m_deps.shrink(target); + for (unsigned i = 0; i < n; i++) + m_frame_bounds.pop_back(); m_kernel.pop(n); }