mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-15 17:49:59 +00:00
Code Activity

Merge pull request #8946 from Z3Prover/copilot/sub-pr-8945

Browse source 
[WIP] [WIP] Address feedback on assertion violation fix in mpz.cpp
This commit is contained in:
Lev Nachmanson 2026-03-11 13:58:40 -10:00 • committed by GitHub
commit 610527ec1a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 86 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

86
src/test/vector.cpp
View file

@ -17,8 +17,92 @@ Revision History:
--*/
#include "util/vector.h"
#include "util/rational.h"
#include <iostream>
static void tst_resize_rational() {
// grow from empty using default initialization (zero)
vector<rational> v;
v.resize(4);
ENSURE(v.size() == 4);
for (unsigned i = 0; i < 4; ++i)
ENSURE(v[i].is_zero());
// shrink: elements below new size are preserved
v.resize(2);
ENSURE(v.size() == 2);
for (unsigned i = 0; i < 2; ++i)
ENSURE(v[i].is_zero());
// grow with explicit value initialization
rational half(1, 2);
v.resize(6, half);
ENSURE(v.size() == 6);
for (unsigned i = 0; i < 2; ++i)
ENSURE(v[i].is_zero());
for (unsigned i = 2; i < 6; ++i)
ENSURE(v[i] == half);
// resize to same size is a no-op
rational three(3);
v.resize(6, three);
ENSURE(v.size() == 6);
for (unsigned i = 2; i < 6; ++i)
ENSURE(v[i] == half);
// resize to zero clears the vector
v.resize(0);
ENSURE(v.empty());
// grow again after being empty
rational neg(-7);
v.resize(3, neg);
ENSURE(v.size() == 3);
for (unsigned i = 0; i < 3; ++i)
ENSURE(v[i] == neg);
}
static void tst_resize() {
// grow from empty using default initialization
svector<int> v;
v.resize(5);
ENSURE(v.size() == 5);
ENSURE(v.capacity() >= 5);
for (unsigned i = 0; i < 5; ++i)
ENSURE(v[i] == 0);
// shrink: elements below new size are preserved, size shrinks
v.resize(3);
ENSURE(v.size() == 3);
for (unsigned i = 0; i < 3; ++i)
ENSURE(v[i] == 0);
// grow with explicit value initialization
v.resize(7, 42);
ENSURE(v.size() == 7);
for (unsigned i = 0; i < 3; ++i)
ENSURE(v[i] == 0);
for (unsigned i = 3; i < 7; ++i)
ENSURE(v[i] == 42);
// resize to same size is a no-op
v.resize(7, 99);
ENSURE(v.size() == 7);
for (unsigned i = 3; i < 7; ++i)
ENSURE(v[i] == 42);
// resize to zero clears the vector
v.resize(0);
ENSURE(v.empty());
ENSURE(v.size() == 0);
// grow again after being empty
v.resize(4, 10);
ENSURE(v.size() == 4);
for (unsigned i = 0; i < 4; ++i)
ENSURE(v[i] == 10);
}
static void tst1() {
svector<int> v1;
ENSURE(v1.empty());
@ -58,5 +142,7 @@ static void tst1() {
}
void tst_vector() {
tst_resize_rational();
tst_resize();
tst1();
}