From 1ec07ac5e99dc211861d70da1164ee31bb8983e0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 30 Mar 2026 19:53:23 -1000 Subject: [PATCH] restore an optimization in scoped_numeral_vector.h Signed-off-by: Lev Nachmanson --- src/util/scoped_numeral_vector.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/scoped_numeral_vector.h b/src/util/scoped_numeral_vector.h index bd4f130f1..44e625550 100644 --- a/src/util/scoped_numeral_vector.h +++ b/src/util/scoped_numeral_vector.h @@ -27,7 +27,7 @@ public: _scoped_numeral_vector(Manager & m):m_manager(m) {} _scoped_numeral_vector(const _scoped_numeral_vector & other) : m_manager(other.m_manager) { - for (unsigned i = 0; i < other.size(); ++i) { + for (unsigned i = 0, e = other.size(); i != e; ++i) { push_back(other[i]); } }