mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
add unit test for previous commit
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
parent
c824178e7e
commit
7e0723e42b
|
@ -276,12 +276,35 @@ static void tst_bv_reset() {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
static void tst_eq() {
|
||||||
|
bit_vector b1, b2, b3;
|
||||||
|
b1.resize(32);
|
||||||
|
b2.resize(32);
|
||||||
|
b3.resize(32);
|
||||||
|
|
||||||
|
b1.set(3, true);
|
||||||
|
SASSERT(b1 != b2);
|
||||||
|
SASSERT(!(b1 == b2));
|
||||||
|
SASSERT(b2 == b3);
|
||||||
|
|
||||||
|
b3.set(3, true);
|
||||||
|
SASSERT(b1 == b3);
|
||||||
|
SASSERT(!(b1 != b3));
|
||||||
|
|
||||||
|
b2.set(31, true);
|
||||||
|
b3.set(31);
|
||||||
|
b3.unset(3);
|
||||||
|
SASSERT(b2 == b3);
|
||||||
|
SASSERT(!(b2 != b3));
|
||||||
|
}
|
||||||
|
|
||||||
void tst_bit_vector() {
|
void tst_bit_vector() {
|
||||||
tst_crash();
|
tst_crash();
|
||||||
tst_shift();
|
tst_shift();
|
||||||
tst_or();
|
tst_or();
|
||||||
tst_and();
|
tst_and();
|
||||||
tst_bv_reset();
|
tst_bv_reset();
|
||||||
|
tst_eq();
|
||||||
return;
|
return;
|
||||||
tst2();
|
tst2();
|
||||||
for (unsigned i = 0; i < 20; i++) {
|
for (unsigned i = 0; i < 20; i++) {
|
||||||
|
|
Loading…
Reference in a new issue