mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 22:04:53 +00:00
Code Activity

Fix invalid zero representation in set_big_i64 and set_big_ui64

Browse source 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-15 22:48:21 +00:00 • committed by Nuno Lopes
parent fa73827d98
commit 04f07fe1d5
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/util/mpz.cpp
View file

@ -259,6 +259,10 @@ void mpz_manager<SYNCH>::sub(mpz const & a, mpz const & b, mpz & c) {
template<bool SYNCH>
void mpz_manager<SYNCH>::set_big_i64(mpz & c, int64_t v) {
if (v == 0) {
set(c, 0);
return;
}
uint64_t _v;
bool sign = v < 0;
if (v == std::numeric_limits<int64_t>::min()) {
@ -309,6 +313,10 @@ void mpz_manager<SYNCH>::set_big_i64(mpz & c, int64_t v) {
template<bool SYNCH>
void mpz_manager<SYNCH>::set_big_ui64(mpz & c, uint64_t v) {
if (v == 0) {
set(c, 0);
return;
}
#ifndef _MP_GMP
if (c.is_small()) {
c.set_ptr(allocate(m_init_cell_capacity), false, false); // positive, owned