From bd993ca9630d7ff1b264f6200e691e3cabe6acce Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Sun, 15 Feb 2026 16:45:38 +0000
Subject: [PATCH] fix

---
 src/util/mpq.h      |  3 +++
 src/util/mpz.h      | 11 +++++++++++
 src/util/rational.h |  8 +++++---
 3 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/util/mpq.h b/src/util/mpq.h
index cef964a9e..ff92915a6 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -672,8 +672,11 @@ public:
         set(target.m_den, source.m_den);
     }
 
+    void set(mpz & a, int val) { mpz_manager<SYNCH>::set(a, val); }
     void set(mpz & a, int64_t val) { mpz_manager<SYNCH>::set(a, val); }
 
+    void set(mpq & a, int val) { set(a, (int64_t)val); }
+
     void set(mpq & a, int64_t val) {
         set(a.m_num, val);
         reset_denominator(a);
diff --git a/src/util/mpz.h b/src/util/mpz.h
index c4ac37d1d..4f12b848b 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -159,6 +159,14 @@ public:
         SASSERT(fits_in_small(v));
     }
 
+    mpz(int v) noexcept : m_value(static_cast<uintptr_t>(v) << 1) {
+        SASSERT(fits_in_small(v));
+    }
+
+    mpz(unsigned v) noexcept : m_value(static_cast<uintptr_t>(v) << 1) {
+        SASSERT(fits_in_small(v));
+    }
+
     mpz(mpz_type* ptr) noexcept {
         set_ptr(ptr, false, true); // external pointer, non-negative
     }
@@ -600,6 +608,9 @@ public:
 
     void set(mpz & a, char const * val);
 
+    void set(mpz & a, int val)      { set(a, (int64_t)val); }
+    void set(mpz & a, unsigned val) { set(a, (uint64_t)val); }
+
     void set(mpz & a, int64_t val) {
         if (mpz::fits_in_small(val) && is_small(a)) {
             a.set(val);
diff --git a/src/util/rational.h b/src/util/rational.h
index d13b691e1..b74901b0e 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -46,6 +46,8 @@ public:
     rational(rational const & r) { m().set(m_val, r.m_val); }
     rational(rational&&) = default;
 
+    explicit rational(int n) { m().set(m_val, n); }
+    explicit rational(unsigned n) { m().set(m_val, n); }
     explicit rational(int64_t n) { m().set(m_val, n); }
     explicit rational(uint64_t n) { m().set(m_val, n); }
 
@@ -289,7 +291,7 @@ public:
         rational r = mod(a,b);
         SASSERT(r.is_nonneg());
         rational r2 = r;
-        r2 *= rational(uint64_t(2));
+        r2 *= rational(2);
         if (operator<(b, r2)) {
             r -= b;
         }
@@ -509,11 +511,11 @@ public:
     }
 
     unsigned get_num_bits() const {
-        return get_num_digits(rational(uint64_t(2)));
+        return get_num_digits(rational(2));
     }
 
     unsigned get_num_decimal() const {
-        return get_num_digits(rational(uint64_t(10)));
+        return get_num_digits(rational(10));
     }
 
     /**