diff --git a/src/util/rational.h b/src/util/rational.h
index ba447fca6..4fa3382ec 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -52,6 +52,9 @@ public:
 
     rational(mpz const & z) { m().set(m_val, z); }
 
+    rational(double  z) { UNREACHABLE(); }
+
+    
     explicit rational(char const * v) { m().set(m_val, v); }
 
     struct i64 {};
@@ -127,6 +130,12 @@ public:
         return *this;
     }
 
+    rational & operator=(int v) {
+        *this = rational(v);
+        return *this;
+    }
+    rational & operator=(double v) { UNREACHABLE(); return *this; }
+
     friend inline rational numerator(rational const & r) { rational result; m().get_numerator(r.m_val, result.m_val); return result; }
     
     friend inline rational denominator(rational const & r) { rational result; m().get_denominator(r.m_val, result.m_val); return result; }
@@ -136,6 +145,11 @@ public:
         return *this; 
     }
 
+    rational & operator+=(int r) {
+        (*this) += rational(r);
+        return *this;
+    }
+
     rational & operator-=(rational const & r) { 
         m().sub(m_val, r.m_val, m_val);
         return *this; 
@@ -394,6 +408,7 @@ public:
         return num_bits;
     }
 
+    
 };
 
 inline bool operator!=(rational const & r1, rational const & r2) { 
@@ -404,6 +419,10 @@ inline bool operator>(rational const & r1, rational const & r2) {
     return operator<(r2, r1); 
 }
 
+inline bool operator<(rational const & r1, int r2) {
+	return r1 < rational(r2);
+}
+
 inline bool operator<=(rational const & r1, rational const & r2) { 
     return !operator>(r1, r2); 
 }
@@ -412,14 +431,43 @@ inline bool operator>=(rational const & r1, rational const & r2) {
     return !operator<(r1, r2); 
 }
 
+inline bool operator>(rational const & a, int b) {
+    return a > rational(b);
+}
+
+inline bool operator!=(rational const & a, int b) {
+    return !(a == rational(b));
+}
+
+inline bool operator==(rational const & a, int b) {
+    return a == rational(b);
+}
+
 inline rational operator+(rational const & r1, rational const & r2) { 
     return rational(r1) += r2; 
 }
 
+inline rational operator+(int r1, rational const & r2) {
+	return rational(r1) + r2;
+}
+
+inline rational operator+(rational const & r1, int r2) {
+	return r1 + rational(r2);
+}
+
+
 inline rational operator-(rational const & r1, rational const & r2) { 
     return rational(r1) -= r2; 
 }
 
+inline rational operator-(rational const & r1, int r2) {
+	return r1 - rational(r2);
+}
+
+inline rational operator-(int r1, rational const & r2) {
+	return rational(r1) - r2;
+}
+
 inline rational operator-(rational const & r) { 
     rational result(r); 
     result.neg(); 
@@ -430,10 +478,25 @@ inline rational operator*(rational const & r1, rational const & r2) {
     return rational(r1) *= r2; 
 }
 
+inline rational operator*(rational const & r1, int r2) {
+    return r1 * rational(r2);
+}
+inline rational operator*(int  r1, rational const & r2) {
+    return rational(r1) * r2;
+}
+
 inline rational operator/(rational const & r1, rational const & r2) { 
     return rational(r1) /= r2; 
 }
 
+inline rational operator/(rational const & r1, int r2) {
+	return r1 / rational(r2);
+}
+
+inline rational operator/(int r1, rational const &	r2) {
+	return rational(r1) / r2;
+}
+
 inline rational power(rational const & r, unsigned p) {
     return r.expt(p);
 }