mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 06:07:46 +00:00
Code Activity

use shrink instead of pop in a loop

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-05-16 10:29:45 -07:00
parent b8052d67cb
commit 5ca32d65bd
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/nseq_context_solver.h
View file

@ -125,7 +125,6 @@ namespace smt {
void pop(unsigned n) override { void pop(unsigned n) override {
SASSERT(n <= m_frame_bounds.size()); SASSERT(n <= m_frame_bounds.size());
unsigned target = m_frame_bounds[m_frame_bounds.size() - n]; unsigned target = m_frame_bounds[m_frame_bounds.size() - n];
while (m_deps.size() > target) {
m_deps.pop_back(); m_deps.pop_back();
} }
for (unsigned i = 0; i < n; i++) { for (unsigned i = 0; i < n; i++) {