mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-22 01:49:36 +00:00
Code Activity

Fix uninitialized and array-bounds build warnings

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/ee8157b2-c614-4b32-b54b-ecfa0afcbf9f

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-13 10:40:59 +00:00 • committed by GitHub
parent 2f7ff62173
commit bba87df6df
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/simplifiers/bound_propagator.cpp
View file

@ -381,7 +381,7 @@ bool bound_propagator::relevant_bound(var x, double new_k) const {
if (b == nullptr) if (b == nullptr)
return true; // variable did not have a bound return true; // variable did not have a bound
double interval_size; double interval_size = 0.0;
bool bounded = get_interval_size(x, interval_size); bool bounded = get_interval_size(x, interval_size);
if (!is_int(x)) { if (!is_int(x)) {
@ -939,4 +939,3 @@ void bound_propagator::display(std::ostream & out) const {
} }

5
src/util/mpz.h
View file

@ -314,13 +314,14 @@ class mpz_manager {
else { else {
cell = reserve; cell = reserve;
cell->m_size = 1; cell->m_size = 1;
digit_t* cell_digits = reinterpret_cast<digit_t*>(cell + 1);
if (a.value() < 0) { if (a.value() < 0) {
sign = -1; sign = -1;
cell->m_digits[0] = -a.value(); cell_digits[0] = -a.value();
} }
else { else {
sign = 1; sign = 1;
cell->m_digits[0] = a.value(); cell_digits[0] = a.value();
} }
} }
} }