mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 06:52:26 +00:00
Code Activity

Add widened vector growth arithmetic and regression test

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-08-07 06:55:15 +00:00 • committed by GitHub
parent a37f306cb4
commit 04e0f3b024
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/test/vector.cpp
View file

@ -144,9 +144,10 @@ static void tst1() {
static void tst_expand_vector_byte_count() {
vector<uint16_t, true, uint8_t> v;
for (unsigned i = 0; i < 192; ++i)
// 191 forces growth from capacity 127 -> 191 where byte-size exceeds uint8_t.
for (unsigned i = 0; i < 191; ++i)
v.push_back(i);
ENSURE(v.size() == 192);
ENSURE(v.size() == 191);
}
void tst_vector() {

6
src/util/vector.h
View file

@ -28,6 +28,7 @@ Revision History:
#include "util/debug.h"
#include <algorithm>
#include <functional>
#include <limits>
#include <memory>
#include <type_traits>
#include <utility>
@ -81,7 +82,10 @@ class vector {
SASSERT(capacity() > 0);
SZ old_capacity = reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
size_t old_capacity_T = sizeof(T) * static_cast<size_t>(old_capacity) + sizeof(SZ) * 2;
SZ new_capacity = (3 * old_capacity + 1) >> 1;
size_t grown_capacity = (3 * static_cast<size_t>(old_capacity) + 1) >> 1;
if (grown_capacity > std::numeric_limits<SZ>::max())
throw default_exception("Overflow encountered when expanding vector");
SZ new_capacity = static_cast<SZ>(grown_capacity);
size_t new_capacity_T = sizeof(T) * static_cast<size_t>(new_capacity) + sizeof(SZ) * 2;
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
throw default_exception("Overflow encountered when expanding vector");