diff --git a/src/nagini_translation/lib/constants.py b/src/nagini_translation/lib/constants.py
index 2c0315bd..dcf186af 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__',
+    '__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..741a4bd0 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/float.sil b/src/nagini_translation/resources/float.sil
index 309fb7c2..a6012d18 100644
--- a/src/nagini_translation/resources/float.sil
+++ b/src/nagini_translation/resources/float.sil
@@ -14,28 +14,28 @@ function float___ge__(self: Ref, other: Ref): Bool
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==>
-            (result == int___ge__(int___unbox__(self), int___unbox__(other)))
+            (result == int___ge__(self, other))
 
 function float___gt__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==>
-            (result == int___gt__(int___unbox__(self), int___unbox__(other)))
+            (result == int___gt__(self, other))
 
 function float___le__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==>
-            (result == int___le__(int___unbox__(self), int___unbox__(other)))
+            (result == int___le__(self, other))
 
 function float___lt__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==>
-            (result == int___lt__(int___unbox__(self), int___unbox__(other)))
+            (result == int___lt__(self, other))
 
 function float___eq__(self: Ref, other: Ref): Bool
     decreases _
diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index
index 65db3ca1..5569bda4 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": ["int___unbox__", "float___ge__"]
         },
         "__gt__": {
-            "args": ["__prim__int", "__prim__int"],
-            "type": "__prim__bool"
+            "args": ["int", "float"],
+            "type": "__prim__bool",
+            "requires": ["int___unbox__", "float___gt__"]
         },
         "__lt__": {
-            "args": ["__prim__int", "__prim__int"],
-            "type": "__prim__bool"
+            "args": ["int", "float"],
+            "type": "__prim__bool",
+            "requires": ["int___unbox__", "float___lt__"]
         },
         "__le__": {
-            "args": ["__prim__int", "__prim__int"],
-            "type": "__prim__bool"
+            "args": ["int", "float"],
+            "type": "__prim__bool",
+            "requires": ["int___unbox__", "float___le__"]
         },
         "__int__": {
             "args": ["int"],
diff --git a/src/nagini_translation/sif/resources/all.sil b/src/nagini_translation/sif/resources/all.sil
index bfda3a22..3d9388b7 100644
--- a/src/nagini_translation/sif/resources/all.sil
+++ b/src/nagini_translation/sif/resources/all.sil
@@ -15,6 +15,7 @@ domain SIFDomain[T] {
 }
 
 import "../../resources/bool.sil"
+import "../../resources/float.sil"
 import "references.sil"
 import "../../resources/bytes.sil"
 import "../../resources/iterator.sil"
diff --git a/src/nagini_translation/sif/resources/preamble.index b/src/nagini_translation/sif/resources/preamble.index
index 4f8551d2..9bcc2026 100644
--- a/src/nagini_translation/sif/resources/preamble.index
+++ b/src/nagini_translation/sif/resources/preamble.index
@@ -257,20 +257,24 @@
             "type": "__prim__int"
         },
         "__ge__": {
-            "args": ["__prim__int", "__prim__int"],
-            "type": "__prim__bool"
+            "args": ["int", "float"],
+            "type": "__prim__bool",
+            "requires": ["int___unbox__", "float___ge__"]
         },
         "__gt__": {
-            "args": ["__prim__int", "__prim__int"],
-            "type": "__prim__bool"
+            "args": ["int", "float"],
+            "type": "__prim__bool",
+            "requires": ["int___unbox__", "float___gt__"]
         },
         "__lt__": {
-            "args": ["__prim__int", "__prim__int"],
-            "type": "__prim__bool"
+            "args": ["int", "float"],
+            "type": "__prim__bool",
+            "requires": ["int___unbox__", "float___lt__"]
         },
         "__le__": {
-            "args": ["__prim__int", "__prim__int"],
-            "type": "__prim__bool"
+            "args": ["int", "float"],
+            "type": "__prim__bool",
+            "requires": ["int___unbox__", "float___le__"]
         },
         "__int__": {
             "args": ["int"],