diff --git a/src/nagini_translation/lib/constants.py b/src/nagini_translation/lib/constants.py
index 2c0315bd..fe4de51f 100644
--- a/src/nagini_translation/lib/constants.py
+++ b/src/nagini_translation/lib/constants.py
@@ -214,17 +214,43 @@
     '__ge__',
     '__lt__',
     '__le__',
+
     '__add__',
-    '__sub_',
+    '__sub__',
     '__mul__',
+    '__truediv__',
     '__floordiv__',
     '__mod__',
+    '__divmod__',
+    '__pow__',
+    '__lshift__',
+    '__rshift__',
+    '__and__',
+    '__or__',
+    '__xor__',
+
+    '__radd__',
+    '__rsub__',
+    '__rmul__',
+    '__rmatmul__',
+    '__rtruediv__',
+    '__rfloordiv__',
+    '__rmod__',
+    '__rdivmod__',
+    '__rpow__(self,',
+    '__rlshift__',
+    '__rrshift__',
+    '__rand__',
+    '__rxor__',
+    '__ror__',
+
     '__init__',
     '__enter__',
     '__exit__',
     '__str__',
     '__len__',
     '__bool__',
+
     '__getitem__',
     '__setitem__',
 }
diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil
index f25a0444..0c60fee4 100644
--- a/src/nagini_translation/resources/bool.sil
+++ b/src/nagini_translation/resources/bool.sil
@@ -68,28 +68,44 @@ function bool___eq__(self: Ref, other: Ref): Bool
     ensures result == object___eq__(self, other)
 
 
-function int___ge__(self: Int, other: Int): Bool
+function int___ge__(self: Ref, other: Ref): Bool
     decreases _
+    requires issubtype(typeof(self), int())
+    requires issubtype(typeof(other), float())
 {
-    self >= other
+    issubtype(typeof(other), int())
+        ? int___unbox__(self) >= int___unbox__(other)
+        : float___ge__(self, other)
 }
 
-function int___gt__(self: Int, other: Int): Bool
+function int___gt__(self: Ref, other: Ref): Bool
     decreases _
+    requires issubtype(typeof(self), int())
+    requires issubtype(typeof(other), float())
 {
-    self > other
+    issubtype(typeof(other), int())
+        ? int___unbox__(self) >= int___unbox__(other)
+        : float___gt__(self, other)
 }
 
-function int___le__(self: Int, other: Int): Bool
+function int___le__(self: Ref, other: Ref): Bool
     decreases _
+    requires issubtype(typeof(self), int())
+    requires issubtype(typeof(other), float())
 {
-    self <= other
+    issubtype(typeof(other), int())
+        ? int___unbox__(self) >= int___unbox__(other)
+        : float___le__(self, other)
 }
 
-function int___lt__(self: Int, other: Int): Bool
+function int___lt__(self: Ref, other: Ref): Bool
     decreases _
+    requires issubtype(typeof(self), int())
+    requires issubtype(typeof(other), float())
 {
-    self < other
+    issubtype(typeof(other), int())
+        ? int___unbox__(self) >= int___unbox__(other)
+        : float___lt__(self, other)
 }
 
 function int___add__(self: Int, other: Int): Int
diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index
index 65db3ca1..33414dab 100644
--- a/src/nagini_translation/resources/preamble.index
+++ b/src/nagini_translation/resources/preamble.index
@@ -254,20 +254,24 @@
             "type": "__prim__int"
         },
         "__ge__": {
-            "args": ["__prim__int", "__prim__int"],
-            "type": "__prim__bool"
+            "args": ["int", "float"],
+            "type": "__prim__bool",
+            "requires": []
         },
         "__gt__": {
-            "args": ["__prim__int", "__prim__int"],
-            "type": "__prim__bool"
+            "args": ["int", "float"],
+            "type": "__prim__bool",
+            "requires": []
         },
         "__lt__": {
-            "args": ["__prim__int", "__prim__int"],
-            "type": "__prim__bool"
+            "args": ["int", "float"],
+            "type": "__prim__bool",
+            "requires": []
         },
         "__le__": {
-            "args": ["__prim__int", "__prim__int"],
-            "type": "__prim__bool"
+            "args": ["int", "float"],
+            "type": "__prim__bool",
+            "requires": []
         },
         "__int__": {
             "args": ["int"],