From 46bc45d904f098ca98b7cac947ea227eda3bbe98 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 9 Feb 2026 18:30:29 +0000 Subject: [PATCH] Add assertion to set() method and simplify get_sign_cell by removing redundant SMALL_INT_MIN case Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com> --- src/util/mpz.h | 16 ++-------------- 1 file changed, 2 insertions(+), 14 deletions(-) diff --git a/src/util/mpz.h b/src/util/mpz.h index 51f1e0d68..68bae1914 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -185,6 +185,7 @@ public: } void set(int v) { + SASSERT(is_small()); m_value = static_cast(static_cast(v)) << 1; } @@ -408,20 +409,7 @@ class mpz_manager { if (is_small(a)) { int64_t val = a.value64(); cell = reserve; - if (val == mpz::SMALL_INT_MIN) { - sign = -1; - uint64_t abs_val = static_cast(-val); - if (sizeof(digit_t) == sizeof(uint64_t)) { - cell->m_size = 1; - cell->m_digits[0] = static_cast(abs_val); - } - else { - cell->m_digits[0] = static_cast(abs_val); - cell->m_digits[1] = static_cast(abs_val >> 32); - cell->m_size = (abs_val >> 32) == 0 ? 1 : 2; - } - } - else if (val < 0) { + if (val < 0) { sign = -1; uint64_t abs_val = static_cast(-val); if (sizeof(digit_t) == sizeof(uint64_t)) {