diff --git a/src/util/mpq.h b/src/util/mpq.h
index ff92915a6..03a51d7d1 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -673,20 +673,17 @@ public:
     }
 
     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) {
+    void set(mpq & a, int val) {
         set(a.m_num, val);
         reset_denominator(a);
     }
 
-    void set(mpq & a, int64_t n, int64_t d) {
+    void set(mpq & a, int n, int d) {
         SASSERT(d != 0);
         if (d < 0) {
-            SASSERT(d != std::numeric_limits<int64_t>());
-            SASSERT(n != std::numeric_limits<int64_t>());
+            SASSERT(d != INT_MIN);
+            SASSERT(n != INT_MIN);
             n = -n;
             d = -d;
         }
@@ -727,6 +724,13 @@ public:
 
     void set(mpq & a, char const * val);
 
+    void set(mpz & a, int64_t val) { mpz_manager<SYNCH>::set(a, val); }
+
+    void set(mpq & a, int64_t val) {
+        set(a.m_num, val);
+        reset_denominator(a);
+    }
+
     void set(mpz & a, uint64_t val) { mpz_manager<SYNCH>::set(a, val); }
     
     void set(mpq & a, uint64_t val) {
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 52441ae38..ef6f5a3c6 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -236,7 +236,7 @@ template<bool SYNCH>
 void mpz_manager<SYNCH>::add(mpz const & a, mpz const & b, mpz & c) {
     STRACE(mpz, tout << "[mpz] " << to_string(a) << " + " << to_string(b) << " == ";); 
     if (is_small(a) && is_small(b)) {
-        set_i64(c, i64(a) + i64(b));
+        set(c, a.value() + b.value());
     }
     else {
         big_add(a, b, c);
@@ -248,7 +248,7 @@ template<bool SYNCH>
 void mpz_manager<SYNCH>::sub(mpz const & a, mpz const & b, mpz & c) {
     STRACE(mpz, tout << "[mpz] " << to_string(a) << " - " << to_string(b) << " == ";); 
     if (is_small(a) && is_small(b)) {
-        set_i64(c, i64(a) - i64(b));
+        set(c, a.value() - b.value());
     }
     else {
         big_sub(a, b, c);
@@ -425,7 +425,7 @@ void mpz_manager<SYNCH>::set_digits(mpz & target, unsigned sz, digit_t const * d
 #ifndef _MP_GMP
         allocate_if_needed(target, sz);
         memcpy(target.ptr()->m_digits, digits, sizeof(digit_t) * sz);
-        target.set_sign(1):
+        target.set_sign(1);
 #else
         mk_big(target);
         // reset
@@ -448,7 +448,7 @@ template<bool SYNCH>
 void mpz_manager<SYNCH>::mul(mpz const & a, mpz const & b, mpz & c) {
     STRACE(mpz, tout << "[mpz] " << to_string(a) << " * " << to_string(b) << " == ";); 
     if (is_small(a) && is_small(b)) {
-        set_i64(c, i64(a) * i64(b));
+        set(c, a.value() * b.value());
     }
     else {
         big_mul(a, b, c);
@@ -496,10 +496,10 @@ template<bool SYNCH>
 void mpz_manager<SYNCH>::machine_div_rem(mpz const & a, mpz const & b, mpz & q, mpz & r) {
     STRACE(mpz, tout << "[mpz-ext] divrem(" << to_string(a) << ",  " << to_string(b) << ") == ";); 
     if (is_small(a) && is_small(b)) {
-        int64_t _a = i64(a);
-        int64_t _b = i64(b);
-        set_i64(q, _a / _b);
-        set_i64(r, _a % _b);
+        int64_t _a = a.value();
+        int64_t _b = b.value();
+        set(q, _a / _b);
+        set(r, _a % _b);
     }
     else {
         big_div_rem(a, b, q, r);
@@ -510,11 +510,11 @@ void mpz_manager<SYNCH>::machine_div_rem(mpz const & a, mpz const & b, mpz & q,
 template<bool SYNCH>
 void mpz_manager<SYNCH>::machine_div(mpz const & a, mpz const & b, mpz & c) {
     STRACE(mpz, tout << "[mpz-ext] machine-div(" << to_string(a) << ",  " << to_string(b) << ") == ";); 
-    if (is_small(b) && i64(b) == 0)
+    if (is_small(b) && b.value() == 0)
         throw default_exception("division by 0"); 
 
     if (is_small(a) && is_small(b)) 
-        set_i64(c, i64(a) / i64(b));
+        set(c, a.value() / b.value());
     else 
         big_div(a, b, c);
     STRACE(mpz, tout << to_string(c) << "\n";);
@@ -530,7 +530,7 @@ template<bool SYNCH>
 void mpz_manager<SYNCH>::rem(mpz const & a, mpz const & b, mpz & c) {
     STRACE(mpz, tout << "[mpz-ext] rem(" << to_string(a) << ",  " << to_string(b) << ") == ";); 
     if (is_small(a) && is_small(b)) {
-        set_i64(c, i64(a) % i64(b));
+        set(c, a.value() % b.value());
     }
     else {
         big_rem(a, b, c);
@@ -597,8 +597,8 @@ mpz mpz_manager<SYNCH>::mod2k(mpz const & a, unsigned k) {
 
     if (is_small(a) && k < 64) {
         uint64_t mask = ((1ULL << k) - 1);
-        uint64_t uval = static_cast<uint64_t>(i64(a));
-        set_i64(result, static_cast<int64_t>(uval & mask));
+        uint64_t uval = static_cast<uint64_t>(a.value());
+        set(result, static_cast<int64_t>(uval & mask));
         return result;
     }
 
@@ -1425,7 +1425,7 @@ void mpz_manager<SYNCH>::bitwise_xor(mpz const & a, mpz const & b, mpz & c) {
     SASSERT(is_nonneg(a));
     SASSERT(is_nonneg(b));
     if (is_small(a) && is_small(b)) {
-        set_i64(c, i64(a) ^ i64(b));
+        set(c, a.value() ^ b.value());
     }
     else {
 #ifndef _MP_GMP
@@ -1902,9 +1902,9 @@ bool mpz_manager<SYNCH>::is_power_of_two(mpz const & a, unsigned & shift) {
     if (is_nonpos(a))
         return false;
     if (is_small(a)) {
-        int64_t v = a.value();
+        auto v = static_cast<uint64_t>(a.value());
         if (::is_power_of_two(v)) {
-            shift = log2(static_cast<uint64_t>(v));
+            shift = ::log2(v);
             return true;
         }
         else {
@@ -1968,7 +1968,7 @@ void mpz_manager<SYNCH>::ensure_capacity(mpz & a, unsigned capacity) {
         unsigned old_sz  = a.ptr()->m_size;
         SASSERT(capacity >= old_sz);
         new_cell->m_size = old_sz;
-        memcpy(new_cell->m_digits, digits(a), sizeof(digit_t) * old_sz)
+        memcpy(new_cell->m_digits, digits(a), sizeof(digit_t) * old_sz);
         bool is_neg = a.sign() < 0;
         deallocate(a);
         a.set_ptr(new_cell, is_neg, false);
@@ -2063,7 +2063,7 @@ void mpz_manager<SYNCH>::mul2k(mpz & a, unsigned k) {
     if (k == 0 || is_zero(a))
         return;
     if (is_small(a) && k < 32) {
-        set_i64(a, i64(a) * (static_cast<int64_t>(1) << k));
+        set(a, a.value() * (static_cast<int64_t>(1) << k));
         return;
     }
 #ifndef _MP_GMP
@@ -2177,7 +2177,7 @@ unsigned mpz_manager<SYNCH>::mlog2(mpz const & a) {
     if (is_nonneg(a))
         return 0;
     if (is_small(a)) {
-        return ::log2(static_cast<uint64_t>(-va.value()));
+        return ::log2(static_cast<uint64_t>(-a.value()));
     }
 #ifndef _MP_GMP
     static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, "");
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 4f12b848b..1e87f29a9 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -317,8 +317,6 @@ class mpz_manager {
 
     mpz m_two64;
 
-    static int64_t i64(mpz const & a) { return a.value(); }
-
     void set_big_i64(mpz & c, int64_t v);
     void set_big_ui64(mpz & c, uint64_t v);
 
diff --git a/src/util/rational.h b/src/util/rational.h
index b74901b0e..a2354736e 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -51,7 +51,7 @@ public:
     explicit rational(int64_t n) { m().set(m_val, n); }
     explicit rational(uint64_t n) { m().set(m_val, n); }
 
-    rational(int64_t n, int64_t d) { m().set(m_val, n, d); }
+    rational(int n, int d) { m().set(m_val, n, d); }
     rational(mpq const & q) { m().set(m_val, q); }
     rational(mpq && q) noexcept : m_val(std::move(q)) {}
     rational(mpz const & z) { m().set(m_val, z); }
@@ -173,6 +173,7 @@ public:
     rational & operator=(bool) = delete;
     rational operator*(bool  r1) const = delete;
 
+    rational & operator=(int v) { return *this = (int64_t)v; }
     rational & operator=(int64_t v) {
         m().set(m_val, v);
         return *this;
@@ -194,7 +195,7 @@ public:
         return *this; 
     }
 
-    rational & operator+=(int64_t r) {
+    rational & operator+=(int r) {
         (*this) += rational(r);
         return *this;
     }
@@ -204,7 +205,7 @@ public:
         return *this; 
     }
 
-    rational& operator-=(int64_t r) {
+    rational& operator-=(int r) {
         (*this) -= rational(r);
         return *this;
     }
@@ -224,15 +225,15 @@ public:
         return *this; 
     }    
 
-    rational & operator%=(int64_t v) {
+    rational & operator%=(int v) {
         return *this %= rational(v);
     }    
 
-    rational & operator/=(int64_t v) {
+    rational & operator/=(int v) {
         return *this /= rational(v);
     }    
 
-    rational & operator*=(int64_t v) {
+    rational & operator*=(int v) {
         return *this *= rational(v);
     }    
 
@@ -562,11 +563,11 @@ inline bool operator>(rational const & r1, rational const & r2) {
     return operator<(r2, r1); 
 }
 
-inline bool operator<(int64_t r1, rational const & r2) {
+inline bool operator<(int r1, rational const & r2) {
     return rational(r1) < r2;
 }
 
-inline bool operator<(rational const & r1, int64_t r2) {
+inline bool operator<(rational const & r1, int r2) {
     return r1 < rational(r2);
 }
 
@@ -578,35 +579,35 @@ inline bool operator>=(rational const & r1, rational const & r2) {
     return !operator<(r1, r2); 
 }
 
-inline bool operator>(rational const & a, int64_t b) {
+inline bool operator>(rational const & a, int b) {
     return a > rational(b);
 }
 
-inline bool operator>(int64_t a, rational const & b) {
+inline bool operator>(int a, rational const & b) {
     return rational(a) > b;
 }
 
-inline bool operator>=(rational const& a, int64_t b) {
+inline bool operator>=(rational const& a, int b) {
     return a >= rational(b);
 }
 
-inline bool operator>=(int64_t a, rational const& b) {
+inline bool operator>=(int a, rational const& b) {
     return rational(a) >= b;
 }
 
-inline bool operator<=(rational const& a, int64_t b) {
+inline bool operator<=(rational const& a, int b) {
     return a <= rational(b);
 }
 
-inline bool operator<=(int64_t a, rational const& b) {
+inline bool operator<=(int a, rational const& b) {
     return rational(a) <= b;
 }
 
-inline bool operator!=(rational const& a, int64_t b) {
+inline bool operator!=(rational const& a, int b) {
     return !(a == rational(b));
 }
 
-inline bool operator==(rational const & a, int64_t b) {
+inline bool operator==(rational const & a, int b) {
     return a == rational(b);
 }
 
@@ -614,11 +615,11 @@ inline rational operator+(rational const & r1, rational const & r2) {
     return rational(r1) += r2; 
 }
 
-inline rational operator+(int64_t r1, rational const & r2) {
+inline rational operator+(int r1, rational const & r2) {
     return rational(r1) + r2;
 }
 
-inline rational operator+(rational const & r1, int64_t r2) {
+inline rational operator+(rational const & r1, int r2) {
     return r1 + rational(r2);
 }
 
@@ -627,11 +628,11 @@ inline rational operator-(rational const & r1, rational const & r2) {
     return rational(r1) -= r2; 
 }
 
-inline rational operator-(rational const & r1, int64_t r2) {
+inline rational operator-(rational const & r1, int r2) {
     return r1 - rational(r2);
 }
 
-inline rational operator-(int64_t r1, rational const & r2) {
+inline rational operator-(int r1, rational const & r2) {
     return rational(r1) - r2;
 }
 
@@ -647,17 +648,17 @@ inline rational operator*(rational const & r1, rational const & r2) {
 
 inline rational operator*(rational const & r1, bool r2) {
     UNREACHABLE();
-    return r1 * rational((uint64_t)r2);
-}
-inline rational operator*(rational const & r1, int64_t r2) {
     return r1 * rational(r2);
 }
-inline rational operator*(bool r1, rational const & r2) {
+inline rational operator*(rational const & r1, int r2) {
+    return r1 * rational(r2);
+}
+inline rational operator*(bool  r1, rational const & r2) {
     UNREACHABLE();
-    return rational((uint64_t)r1) * r2;
+    return rational(r1) * r2;
 }
 
-inline rational operator*(int64_t r1, rational const & r2) {
+inline rational operator*(int  r1, rational const & r2) {
     return rational(r1) * r2;
 }
 
@@ -665,16 +666,16 @@ inline rational operator/(rational const & r1, rational const & r2) {
     return rational(r1) /= r2; 
 }
 
-inline rational operator/(rational const & r1, int64_t r2) {
+inline rational operator/(rational const & r1, int r2) {
     return r1 / rational(r2);
 }
 
 inline rational operator/(rational const & r1, bool r2) {
     UNREACHABLE();
-    return r1 / rational((uint64_t)r2);
+    return r1 / rational(r2);
 }
 
-inline rational operator/(int64_t r1, rational const &    r2) {
+inline rational operator/(int r1, rational const &    r2) {
     return rational(r1) / r2;
 }