diff --git a/src/nagini_contracts/contracts.py b/src/nagini_contracts/contracts.py
index 38cc3cb6..9e5fcf2b 100644
--- a/src/nagini_contracts/contracts.py
+++ b/src/nagini_contracts/contracts.py
@@ -31,7 +31,7 @@
                   'Acc', 'Rd', 'Wildcard', 'Fold', 'Unfold', 'Unfolding', 'Previous',
                   'RaisedException', 'PSeq', 'PSet', 'ToSeq', 'ToMS', 'MaySet', 'MayCreate',
                   'getMethod', 'getArg', 'getOld', 'arg', 'Joinable', 'MayStart', 'Let',
-                  'PMultiset', 'LowExit', 'Refute']
+                  'PMultiset', 'LowExit', 'Refute', 'isNaN']
 
 T = TypeVar('T')
 V = TypeVar('V')
@@ -506,6 +506,8 @@ def dict_pred(d: object) -> bool:
     be folded or unfolded.
     """
 
+def isNaN(f: float) -> bool:
+    pass
 
 __all__ = [
         'Requires',
@@ -560,4 +562,5 @@ def dict_pred(d: object) -> bool:
         'ToMS',
         'MaySet',
         'MayCreate',
+        'isNaN'
         ]
diff --git a/src/nagini_translation/lib/resolver.py b/src/nagini_translation/lib/resolver.py
index c0063822..d9d26b1d 100644
--- a/src/nagini_translation/lib/resolver.py
+++ b/src/nagini_translation/lib/resolver.py
@@ -461,7 +461,7 @@ def _get_call_type(node: ast.Call, module: PythonModule,
                 return ctx.current_contract_exception
             elif node.func.id in ('Acc', 'Rd', 'Read', 'Implies', 'Forall', 'IOForall', 'Exists',
                                   'Forall2', 'Forall3', 'Forall4', 'Forall5', 'Forall6',
-                                  'MayCreate', 'MaySet', 'Low', 'LowVal', 'LowEvent', 'LowExit'):
+                                  'MayCreate', 'MaySet', 'Low', 'LowVal', 'LowEvent', 'LowExit', 'isNaN'):
                 return module.global_module.classes[BOOL_TYPE]
             elif node.func.id == 'Declassify':
                 return None
diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil
index 31451380..afbd15ba 100644
--- a/src/nagini_translation/resources/bool.sil
+++ b/src/nagini_translation/resources/bool.sil
@@ -40,6 +40,7 @@ function int___unbox__(box: Ref): Int
     requires issubtype(typeof(box), int())
     ensures !issubtype(typeof(box), bool()) ==> __prim__int___box__(result) == box
     ensures issubtype(typeof(box), bool()) ==> __prim__bool___box__(result != 0) == box
+    ensures forall i: Ref :: {object___eq__(box, i), int___unbox__(i)} (object___eq__(box, i) && issubtype(typeof(i), int())) ==> int___unbox__(i) == result
 
 function __prim__bool___box__(prim: Bool): Ref
     decreases _
@@ -55,9 +56,10 @@ function bool___unbox__(box: Ref): Bool
 function int___eq__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), int())
-    requires issubtype(typeof(other), int())
-    ensures result == int___unbox__(self) == int___unbox__(other)
-    ensures result == object___eq__(self, other)
+    requires issubtype(typeof(other), int()) || issubtype(typeof(other), float())
+    ensures issubtype(typeof(other), int()) ==> result == int___unbox__(self) == int___unbox__(other)
+    ensures issubtype(typeof(other), int()) ==> result == object___eq__(self, other)
+    ensures issubtype(typeof(other), float()) ==> result == float___eq__(self, other)
 
 
 function bool___eq__(self: Ref, other: Ref): Bool
diff --git a/src/nagini_translation/resources/float.sil b/src/nagini_translation/resources/float.sil
index 1b00c130..03091d69 100644
--- a/src/nagini_translation/resources/float.sil
+++ b/src/nagini_translation/resources/float.sil
@@ -9,6 +9,11 @@ function float___bool__(self: Ref): Bool
     ensures self == null ==> !result
     ensures issubtype(typeof(self), int()) ==> (result == int___bool__(self))
 
+function float___isNaN(f: Ref): Bool
+    decreases _
+    requires issubtype(typeof(f), float())
+    ensures issubtype(typeof(f), int()) ==> result == false
+
 function float___ge__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())
diff --git a/src/nagini_translation/resources/float_ieee32.sil b/src/nagini_translation/resources/float_ieee32.sil
index 68327fe6..cb9cf479 100644
--- a/src/nagini_translation/resources/float_ieee32.sil
+++ b/src/nagini_translation/resources/float_ieee32.sil
@@ -18,6 +18,11 @@ function float___bool__(self: Ref): Bool
     ensures self == null ==> !result
     ensures result == (float___unbox__(self) != ___float32_zero())
 
+function float___isNaN(f: Ref): Bool
+    decreases _
+    requires issubtype(typeof(f), float())
+    ensures result == ___float32_isNaN(float___unbox__(f)) 
+
 function float___ge__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())
@@ -144,6 +149,7 @@ domain ___float32 interpretation (Boogie: "float24e8", SMTLIB: "(_ FloatingPoint
   function real____to_int(p: Perm): Int interpretation "to_int"
   function ___float32_to_real(p: ___float32): Perm interpretation "fp.to_real"
   function ___float32_NaN(): ___float32 interpretation "(_ NaN 8 24)"
+  function ___float32_isNaN(___float32): Bool interpretation "fp.isNaN"
 }
 
 function ___float32_zero(): ___float32
diff --git a/src/nagini_translation/resources/float_real.sil b/src/nagini_translation/resources/float_real.sil
index e0377b1e..596be318 100644
--- a/src/nagini_translation/resources/float_real.sil
+++ b/src/nagini_translation/resources/float_real.sil
@@ -5,121 +5,418 @@ function float___create__(i: Int): Ref
 function float___unbox__(r: Ref): Perm
     decreases _
     requires issubtype(typeof(r), float())
+    requires float___is_nan__(r) == false
+    requires float___is_inf__(r, false) == false
+    requires float___is_inf__(r, true) == false
     ensures issubtype(typeof(r), int()) ==> result == (int___unbox__(r) / 1)
 
 function __prim__perm___box__(p: Perm): Ref
     decreases _
     ensures typeof(result) == float()
+    ensures float___is_nan__(result) == false
+    ensures float___is_inf__(result, false) == false
+    ensures float___is_inf__(result, true) == false
     ensures float___unbox__(result) == p
 
+function float___box_nan(): Ref
+    decreases _
+    ensures typeof(result) == float()
+    ensures float___is_nan__(result) == true
+    ensures float___is_inf__(result, false) == false
+    ensures float___is_inf__(result, true) == false
+
+function float___box_inf(negative: Bool): Ref
+    decreases _
+    ensures typeof(result) == float()
+    ensures float___is_nan__(result) == false
+    ensures float___is_inf__(result, false) == !negative
+    ensures float___is_inf__(result, true) == negative
+
+function float___is_nan__(r: Ref): Bool
+    decreases _
+    requires issubtype(typeof(r), float())
+    ensures issubtype(typeof(r), int()) ==> result == false
+
+function float___is_inf__(r: Ref, negative: Bool): Bool
+    decreases _
+    requires issubtype(typeof(r), float())
+    ensures issubtype(typeof(r), int()) ==> result == false
+
+function float___isNaN(f: Ref): Bool
+    decreases _
+    requires issubtype(typeof(f), float())
+    ensures result == float___is_nan__(f)
+
 function float___bool__(self: Ref): Bool
     decreases _
-    requires self != null ==> issubtype(typeof(self), float())
-    ensures self == null ==> !result
-    ensures result == (float___unbox__(self) != none)
+    requires issubtype(typeof(self), float())
+    ensures float___is_nan__(self) == false && float___is_inf__(self, false) == false && float___is_inf__(self, true) == false ==>
+        result == (float___unbox__(self) != 0 / 1)
+    ensures float___is_nan__(self) == true || float___is_inf__(self, false) == true || float___is_inf__(self, true) == true ==>
+        result == true
 
 function float___ge__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    ensures result == (float___unbox__(self) >= float___unbox__(other))
+    ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
+        result == false
+    ensures float___is_inf__(self, false) == true ==> result == true
+    ensures float___is_inf__(self, true) == true ==> result == (float___is_inf__(other, true) == true)
+    ensures float___is_inf__(other, false) == true ==> result == (float___is_inf__(self, false) == true)
+    ensures float___is_inf__(other, true) == true ==> result == true
+    ensures float___is_nan__(self) == false && float___is_nan__(other) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==>
+        result == (float___unbox__(self) >= float___unbox__(other))
 
 function float___gt__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    ensures result == (float___unbox__(self) > float___unbox__(other))
+    ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
+        result == false
+    ensures float___is_inf__(self, false) == true ==> result == (float___is_inf__(other, false) == false)
+    ensures float___is_inf__(self, true) == true ==> result == false
+    ensures float___is_inf__(other, false) == true ==> result == false
+    ensures float___is_inf__(other, true) == true ==> result == (float___is_inf__(self, true) == false)
+    ensures float___is_nan__(self) == false && float___is_nan__(other) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==>
+        result == (float___unbox__(self) > float___unbox__(other))
 
 function float___le__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    ensures result == (float___unbox__(self) <= float___unbox__(other))
+    ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
+        result == false
+    ensures float___is_inf__(self, false) == true ==> result == (float___is_inf__(other, false) == true)
+    ensures float___is_inf__(self, true) == true ==> result == true
+    ensures float___is_inf__(other, false) == true ==> result == true
+    ensures float___is_inf__(other, true) == true ==> result == (float___is_inf__(self, true) == true)
+    ensures float___is_nan__(self) == false && float___is_nan__(other) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==>
+        result == (float___unbox__(self) <= float___unbox__(other))
 
 function float___lt__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    ensures result == (float___unbox__(self) < float___unbox__(other))
+    ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
+        result == false
+    ensures float___is_inf__(self, false) == true ==> result == false
+    ensures float___is_inf__(self, true) == true ==> result == (float___is_inf__(other, true) == false)
+    ensures float___is_inf__(other, false) == true ==> result == (float___is_inf__(self, false) == false)
+    ensures float___is_inf__(other, true) == true ==> result == false
+    ensures float___is_nan__(self) == false && float___is_nan__(other) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==>
+        result == (float___unbox__(self) < float___unbox__(other))
 
 function float___eq__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    ensures result == (float___unbox__(self) == float___unbox__(other))
+    ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
+        result == false
+    ensures (float___is_inf__(self, false) == true && float___is_inf__(other, false) == true) ||
+            (float___is_inf__(self, true) == true && float___is_inf__(other, true) == true) ==>
+                result == true
+    ensures (float___is_inf__(self, false) == true && float___is_inf__(other, false) == false) ||
+           (float___is_inf__(self, true) == true  && float___is_inf__(other, true) == false) ||
+           (float___is_inf__(other, false) == true && float___is_inf__(self, false) == false) ||
+           (float___is_inf__(other, true) == true && float___is_inf__(self, true) == false) ==>
+               result == false
+    ensures (float___is_nan__(self) == false && float___is_nan__(other) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false) ==>
+            result == (float___unbox__(self) == float___unbox__(other))
 
 function float___add__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     ensures issubtype(typeof(result), float())
-    ensures result == __prim__perm___box__(float___unbox__(self) + float___unbox__(other))
+    ensures (float___is_nan__(self) == true || float___is_nan__(other) == true) ==>
+        result == float___box_nan()
+    ensures ((float___is_inf__(self, false) == true && float___is_inf__(other, true) == true) ||
+            (float___is_inf__(self, true) == true && float___is_inf__(other, false) == true)) ==>
+                (result == float___box_nan())
+    ensures ((float___is_inf__(self, false) == true && float___is_inf__(other, true) == false && float___is_nan__(other) == false) ||
+            (float___is_inf__(other, false) == true && float___is_inf__(self, true) == false && float___is_nan__(self) == false)) ==>
+                (result == float___box_inf(false))
+    ensures ((float___is_inf__(self, true) == true && float___is_inf__(other, false) == false && float___is_nan__(other) == false) ||
+            (float___is_inf__(other, true) == true && float___is_inf__(self, false) == false && float___is_nan__(self) == false)) ==>
+                (result == float___box_inf(true))
+    ensures (float___is_nan__(self) == false && float___is_nan__(other) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false) ==>
+        (result == __prim__perm___box__(float___unbox__(self) + float___unbox__(other)))
 
 function float___radd__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     ensures issubtype(typeof(result), float())
-    ensures result == __prim__perm___box__(float___unbox__(other) + float___unbox__(self))
+    ensures (float___is_nan__(self) == true || float___is_nan__(other) == true) ==>
+        result == float___box_nan()
+    ensures ((float___is_inf__(self, false) == true && float___is_inf__(other, true) == true) ||
+            (float___is_inf__(self, true) == true && float___is_inf__(other, false) == true)) ==>
+                result == float___box_nan()
+    ensures ((float___is_inf__(self, false) == true && float___is_inf__(other, true) == false && float___is_nan__(other) == false) ||
+            (float___is_inf__(other, false) == true && float___is_inf__(self, true) == false && float___is_nan__(self) == false)) ==>
+                result == float___box_inf(false)
+    ensures ((float___is_inf__(self, true) == true && float___is_inf__(other, false) == false && float___is_nan__(other) == false) ||
+            (float___is_inf__(other, true) == true && float___is_inf__(self, false) == false && float___is_nan__(self) == false)) ==>
+                result == float___box_inf(true)
+    ensures (float___is_nan__(self) == false && float___is_nan__(other) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false) ==>
+        result == __prim__perm___box__(float___unbox__(other) + float___unbox__(self))
 
 function float___sub__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     ensures issubtype(typeof(result), float())
-    ensures result == __prim__perm___box__(float___unbox__(self) - float___unbox__(other))
+    ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
+        result == float___box_nan()
+    ensures (float___is_inf__(self, false) == true && float___is_inf__(other, false) == true) ||
+            (float___is_inf__(self, true) == true && float___is_inf__(other, true) == true) ==>
+                result == float___box_nan()
+    ensures (float___is_inf__(self, false) == true && float___is_inf__(other, false) == false && float___is_nan__(other) == false)  ||
+            (float___is_inf__(self, false) == false && float___is_inf__(self, true) == false && float___is_nan__(self) == false && float___is_inf__(other, true) == true) ==>
+                result == float___box_inf(false)
+    ensures (float___is_inf__(self, true) == true && float___is_inf__(other, true) == false && float___is_nan__(other) == false) ||
+            (float___is_inf__(self, false) == false && float___is_inf__(self, true) == false && float___is_nan__(self) == false && float___is_inf__(other, false) == true) ==>
+                result == float___box_inf(true)
+    ensures float___is_nan__(self) == false && float___is_nan__(other) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==>
+        result == __prim__perm___box__(float___unbox__(self) - float___unbox__(other))
 
 function float___rsub__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     ensures issubtype(typeof(result), float())
-    ensures result == __prim__perm___box__(float___unbox__(other) - float___unbox__(self))
+    ensures float___is_nan__(other) == true || float___is_nan__(self) == true ==>
+        result == float___box_nan()
+    ensures (float___is_inf__(other, false) == true && float___is_inf__(self, false) == true) ||
+            (float___is_inf__(other, true) == true && float___is_inf__(self, true) == true) ==>
+                result == float___box_nan()
+    ensures (float___is_inf__(other, false) == true && float___is_inf__(self, false) == false && float___is_nan__(self) == false)  ||
+            (float___is_inf__(other, false) == false && float___is_inf__(other, true) == false && float___is_nan__(other) == false && float___is_inf__(self, true) == true) ==>
+                result == float___box_inf(false)
+    ensures (float___is_inf__(other, true) == true && float___is_inf__(self, true) == false && float___is_nan__(self) == false) ||
+            (float___is_inf__(other, false) == false && float___is_inf__(other, true) == false && float___is_nan__(other) == false && float___is_inf__(self, false) == true) ==>
+                result == float___box_inf(true)
+    ensures float___is_nan__(other) == false && float___is_nan__(self) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false ==>
+        result == __prim__perm___box__(float___unbox__(other) - float___unbox__(self))
 
 function float___mul__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     ensures issubtype(typeof(result), float())
-    ensures result == __prim__perm___box__(float___unbox__(self) * float___unbox__(other))
+    ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
+        result == float___box_nan()
+    ensures float___is_nan__(self) == false && 
+            float___is_inf__(self, false) == false && 
+            float___is_inf__(self, true) == false &&
+            float___unbox__(self) == 0 / 1 && 
+            (float___is_inf__(other, false) == true || float___is_inf__(other, true) == true) ==>
+                result == float___box_nan()
+    ensures float___is_nan__(other) == false && 
+            float___is_inf__(other, false) == false && 
+            float___is_inf__(other, true) == false &&
+            float___unbox__(other) == 0 / 1 && 
+            (float___is_inf__(self, false) == true || float___is_inf__(self, true) == true) ==>
+                result == float___box_nan()
+    ensures (float___is_inf__(self, false) == true && float___is_inf__(other, false) == true) ||
+            (float___is_inf__(self, true) == true && float___is_inf__(other, true) == true) ==>
+                result == float___box_inf(false)
+    ensures float___is_nan__(self) == false &&
+            float___is_inf__(self, false) == false &&
+            float___is_inf__(self, true) == false &&
+            ((float___unbox__(self) > 0 / 1 && float___is_inf__(other, false) == true) ||
+            (float___unbox__(self) < 0 / 1 && float___is_inf__(other, true) == true)) ==>
+                result == float___box_inf(false)
+    ensures float___is_nan__(other) == false &&
+            float___is_inf__(other, false) == false &&
+            float___is_inf__(other, true) == false &&
+            ((float___is_inf__(self, false) == true && float___unbox__(other) > 0 / 1) ||
+            (float___is_inf__(self, true) == true && float___unbox__(other) < 0 / 1)) ==>
+                result == float___box_inf(false)
+    ensures (float___is_inf__(self, false) == true && float___is_inf__(other, true) == true) ||
+            (float___is_inf__(self, true) == true && float___is_inf__(other, false) == true) ==>
+                result == float___box_inf(true)
+    ensures float___is_nan__(self) == false &&
+            float___is_inf__(self, false) == false &&
+            float___is_inf__(self, true) == false &&
+            ((float___unbox__(self) > 0 / 1 && float___is_inf__(other, true) == true) ||
+            (float___unbox__(self) < 0 / 1 && float___is_inf__(other, false) == true)) ==>
+                result == float___box_inf(true)
+    ensures float___is_nan__(other) == false &&
+            float___is_inf__(other, false) == false &&
+            float___is_inf__(other, true) == false &&
+            ((float___unbox__(other) > 0 / 1 && float___is_inf__(self, true) == true) ||
+            (float___unbox__(other) < 0 / 1 && float___is_inf__(self, false) == true)) ==>
+                result == float___box_inf(true)
+    ensures float___is_nan__(other) == false && float___is_nan__(self) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false ==>
+        result == __prim__perm___box__(float___unbox__(self) * float___unbox__(other))
 
 function float___rmul__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     ensures issubtype(typeof(result), float())
-    ensures result == __prim__perm___box__(float___unbox__(other) * float___unbox__(self))
+    ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
+        result == float___box_nan()
+    ensures float___is_nan__(other) == false && 
+            float___is_inf__(other, false) == false && 
+            float___is_inf__(other, true) == false &&
+            float___unbox__(other) == 0 / 1 && 
+            (float___is_inf__(self, false) == true || float___is_inf__(self, true) == true) ==>
+                result == float___box_nan()
+    ensures float___is_nan__(self) == false && 
+            float___is_inf__(self, false) == false && 
+            float___is_inf__(self, true) == false &&
+            float___unbox__(self) == 0 / 1 && 
+            (float___is_inf__(other, false) == true || float___is_inf__(other, true) == true) ==>
+                result == float___box_nan()
+    ensures (float___is_inf__(other, false) == true && float___is_inf__(self, false) == true) ||
+            (float___is_inf__(other, true) == true && float___is_inf__(self, true) == true) ==>
+                result == float___box_inf(false)
+    ensures float___is_nan__(other) == false &&
+            float___is_inf__(other, false) == false &&
+            float___is_inf__(other, true) == false &&
+            ((float___unbox__(other) > 0 / 1 && float___is_inf__(self, false) == true) ||
+            (float___unbox__(other) < 0 / 1 && float___is_inf__(self, true) == true)) ==>
+                result == float___box_inf(false)
+    ensures float___is_nan__(self) == false &&
+            float___is_inf__(self, false) == false &&
+            float___is_inf__(self, true) == false &&
+            ((float___is_inf__(other, false) == true && float___unbox__(self) > 0 / 1) ||
+            (float___is_inf__(other, true) == true && float___unbox__(self) < 0 / 1)) ==>
+                result == float___box_inf(false)
+    ensures (float___is_inf__(other, false) == true && float___is_inf__(self, true) == true) ||
+            (float___is_inf__(other, true) == true && float___is_inf__(self, false) == true) ==>
+                result == float___box_inf(true)
+    ensures float___is_nan__(other) == false &&
+            float___is_inf__(other, false) == false &&
+            float___is_inf__(other, true) == false &&
+            ((float___unbox__(other) > 0 / 1 && float___is_inf__(self, true) == true) ||
+            (float___unbox__(other) < 0 / 1 && float___is_inf__(self, false) == true)) ==>
+                result == float___box_inf(true)
+    ensures float___is_nan__(self) == false &&
+            float___is_inf__(self, false) == false &&
+            float___is_inf__(self, true) == false &&
+            ((float___unbox__(self) > 0 / 1 && float___is_inf__(other, true) == true) ||
+            (float___unbox__(self) < 0 / 1 && float___is_inf__(other, false) == true)) ==>
+                result == float___box_inf(true)
+    ensures float___is_nan__(self) == false && float___is_nan__(other) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==>
+        result == __prim__perm___box__(float___unbox__(other) * float___unbox__(self))
 
 function float___truediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    requires float___unbox__(other) != none
+    requires float___is_nan__(other) == false && float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==>
+        float___unbox__(other) != 0 / 1
     ensures issubtype(typeof(result), float())
-    ensures result == __prim__perm___box__(float___unbox__(self) / float___unbox__(other))
+    ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
+        result == float___box_nan()
+    ensures (float___is_inf__(self, false) == true && float___is_inf__(other, false) == true) ||
+            (float___is_inf__(self, false) == true && float___is_inf__(other, true) == true) ||
+            (float___is_inf__(self, true) == true && float___is_inf__(other, false) == true) ||
+            (float___is_inf__(self, true) == true && float___is_inf__(other, true) == true) ==>
+                result == float___box_nan()
+    ensures (float___is_inf__(other, false) == true || float___is_inf__(other, true) == true) &&
+            float___is_nan__(self) == false &&
+            float___is_inf__(self, false) == false &&
+            float___is_inf__(self, true) == false ==>
+                result == __prim__perm___box__(0 / 1)
+    ensures float___is_nan__(other) == false &&
+            float___is_inf__(other, false) == false &&
+            float___is_inf__(other, true) == false &&
+            ((float___unbox__(other) > 0 / 1 && float___is_inf__(self, false) == true) ||
+            (float___unbox__(other) < 0 / 1 && float___is_inf__(self, true) == true)) ==>
+                result == float___box_inf(false)
+    ensures float___is_nan__(other) == false &&
+            float___is_inf__(other, false) == false &&
+            float___is_inf__(other, true) == false &&
+            ((float___unbox__(other) > 0 / 1 && float___is_inf__(self, true) == true) ||
+            (float___unbox__(other) < 0 / 1 && float___is_inf__(self, false) == true)) ==>
+                result == float___box_inf(true)
+    ensures float___is_nan__(self) == false && float___is_nan__(other) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==>
+        result == __prim__perm___box__(float___unbox__(self) / float___unbox__(other))
 
-function float___pos__(self: Ref): Ref
+function float___rtruediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
-    ensures result == self
+    requires issubtype(typeof(other), float())
+    requires float___is_nan__(self) == false && float___is_inf__(self, false) == false && float___is_inf__(self, true) == false ==>
+        float___unbox__(self) != 0 / 1
+    ensures issubtype(typeof(result), float())
+    ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
+        result == float___box_nan()
+    ensures (float___is_inf__(other, false) == true && float___is_inf__(self, false) == true) ||
+            (float___is_inf__(other, false) == true && float___is_inf__(self, true) == true) ||
+            (float___is_inf__(other, true) == true && float___is_inf__(self, false) == true) ||
+            (float___is_inf__(other, true) == true && float___is_inf__(self, true) == true) ==>
+                result == float___box_nan()
+    ensures (float___is_inf__(self, false) == true || float___is_inf__(self, true) == true) &&
+            float___is_nan__(other) == false &&
+            float___is_inf__(other, false) == false &&
+            float___is_inf__(other, true) == false ==>
+                result == __prim__perm___box__(0 / 1)
+    ensures float___is_nan__(self) == false &&
+            float___is_inf__(self, false) == false &&
+            float___is_inf__(self, true) == false &&
+            ((float___unbox__(self) > 0 / 1 && float___is_inf__(other, false) == true) ||
+            (float___unbox__(self) < 0 / 1 && float___is_inf__(other, true) == true)) ==>
+                result == float___box_inf(false)
+    ensures float___is_nan__(self) == false &&
+            float___is_inf__(self, false) == false &&
+            float___is_inf__(self, true) == false &&
+            ((float___unbox__(self) > 0 / 1 && float___is_inf__(other, true) == true) ||
+            (float___unbox__(self) < 0 / 1 && float___is_inf__(other, false) == true)) ==>
+                result == float___box_inf(true)
+    ensures float___is_nan__(other) == false && float___is_nan__(self) == false &&
+        float___is_inf__(other, false) == false && float___is_inf__(other, true) == false &&
+        float___is_inf__(self, false) == false && float___is_inf__(self, true) == false ==>
+        result == __prim__perm___box__(float___unbox__(other) / float___unbox__(self))
 
-function float___neg__(self: Ref): Ref
+function float___pos__(self: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
-    ensures issubtype(typeof(result), float())
-    ensures result == __prim__perm___box__(-float___unbox__(self))
+    ensures result == self
 
-function float___rtruediv__(self: Ref, other: Ref): Ref
+function float___neg__(self: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
-    requires issubtype(typeof(other), float())
-    requires float___unbox__(self) != none
     ensures issubtype(typeof(result), float())
-    ensures result == __prim__perm___box__(float___unbox__(other) / float___unbox__(self))
+    ensures float___is_nan__(self) == false && float___is_inf__(self, false) == false && float___is_inf__(self, true) == false ==> result == __prim__perm___box__(-float___unbox__(self))
+    ensures float___is_nan__(self) == true ==> result == float___box_nan()
+    ensures float___is_inf__(self, false) == true ==> result == float___box_inf(true)
+    ensures float___is_inf__(self, true) == true ==> result == float___box_inf(false)
 
 function float___int__(self: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
+    requires float___is_nan__(self) == false
+    requires float___is_inf__(self, false) == false && float___is_inf__(self, true) == false
     ensures typeof(result) == int()
     ensures result == __prim__int___box__(____to_int(float___unbox__(self)))
 
diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index
index 15bd1438..6c6e1ffd 100644
--- a/src/nagini_translation/resources/preamble.index
+++ b/src/nagini_translation/resources/preamble.index
@@ -226,7 +226,7 @@
         "__eq__": {
             "args": ["int", "object"],
             "type": "__prim__bool",
-            "requires": ["__unbox__"]
+            "requires": ["__unbox__", "float___eq__"]
         },
         "__add__": {
             "args": ["__prim__int", "__prim__int"],
@@ -304,77 +304,97 @@
         "__unbox__": {
             "args": ["float"],
             "type": "__prim__perm",
-            "requires": ["int___unbox__"]
+            "requires": ["int___unbox__", "float___is_nan__", "float___is_inf__"]
+        },
+        "__box_nan": {
+            "args": [],
+            "type": "float",
+            "requires": ["float___is_nan__", "float___is_inf__"]
+        },
+        "__box_inf": {
+            "args": ["__prim__bool"],
+            "type": "float",
+            "requires": ["float___is_nan__", "float___is_inf__"]
+        },
+        "__is_nan__": {
+            "args": ["float"],
+            "type": "__prim__bool",
+            "requires": []
+        },
+        "__is_inf__": {
+            "args": ["float", "__prim__bool"],
+            "type": "__prim__bool",
+            "requires": []
         },
         "__bool__": {
             "args": ["float"],
             "type": "__prim__bool",
-            "requires": ["int___bool__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
+            "requires": ["int___bool__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero", "float___is_nan__", "float___is_inf__"]
         },
         "__eq__": {
             "args": ["float", "object"],
             "type": "__prim__bool",
-            "requires": ["int___eq__", "unbox"]
+            "requires": ["int___eq__", "unbox", "float___is_nan__", "float___is_inf__"]
         },
         "__add__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__radd__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__sub__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__rsub__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__mul__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__rmul__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__truediv__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
+            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__rtruediv__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
+            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__ge__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___ge__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___ge__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__gt__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___gt__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___gt__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__lt__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___lt__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___lt__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__le__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___le__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___le__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__pos__": {
             "args": ["float"],
@@ -384,12 +404,17 @@
         "__neg__": {
             "args": ["float"],
             "type": "float",
-            "requires": ["int___neg__", "__prim__perm___box__", "unbox"]
+            "requires": ["int___neg__", "__prim__perm___box__", "unbox", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__int__": {
             "args": ["float"],
             "type": "int",
-            "requires": ["unbox", "__prim__int___box__"]
+            "requires": ["unbox", "__prim__int___box__", "float___is_nan__", "float___is_inf__"]
+        },
+        "__isNaN": {
+            "args": ["float"],
+            "type": "__prim__bool",
+            "requires": ["float___is_nan__", "float___unbox__"]
         }
     },
     "extends": "object"
@@ -632,7 +657,7 @@
         "__box__": {
             "args": ["__prim__perm"],
             "type": "int",
-            "requires": ["float___unbox__"]
+            "requires": ["float___unbox__", "float___is_nan__", "float___is_inf__"]
         }
     }
 },
diff --git a/src/nagini_translation/sif/resources/preamble.index b/src/nagini_translation/sif/resources/preamble.index
index 9e6bfd42..6d5ad243 100644
--- a/src/nagini_translation/sif/resources/preamble.index
+++ b/src/nagini_translation/sif/resources/preamble.index
@@ -229,7 +229,7 @@
         "__eq__": {
             "args": ["int", "object"],
             "type": "__prim__bool",
-            "requires": ["__unbox__"]
+            "requires": ["__unbox__", "float___eq__"]
         },
         "__add__": {
             "args": ["__prim__int", "__prim__int"],
@@ -303,6 +303,31 @@
             "args": ["__prim__int"],
             "type": "float"
         },
+        "__unbox__": {
+            "args": ["float"],
+            "type": "__prim__perm",
+            "requires": ["int___unbox__", "float___is_nan__", "float___is_inf__"]
+        },
+        "__box_nan": {
+            "args": [],
+            "type": "float",
+            "requires": ["float___is_nan__", "float___is_inf__"]
+        },
+        "__box_inf": {
+            "args": ["__prim__bool"],
+            "type": "float",
+            "requires": ["float___is_nan__", "float___is_inf__"]
+        },
+        "__is_nan__": {
+            "args": ["float"],
+            "type": "__prim__bool",
+            "requires": []
+        },
+        "__is_inf__": {
+            "args": ["float", "__prim__bool"],
+            "type": "__prim__bool",
+            "requires": []
+        },
         "__bool__": {
             "args": ["float"],
             "type": "__prim__bool",
@@ -311,47 +336,67 @@
         "__eq__": {
             "args": ["float", "object"],
             "type": "__prim__bool",
-            "requires": ["int___eq__"]
+            "requires": ["int___eq__", "unbox", "float___is_nan__", "float___is_inf__"]
         },
         "__add__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___add__", "int___unbox__"]
+            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
+        },
+        "__radd__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__sub__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___sub__", "int___unbox__"]
+            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
+        },
+        "__rsub__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__mul__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___mul__", "int___unbox__"]
+            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
+        },
+        "__rmul__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__truediv__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___truediv__", "int___unbox__"]
+            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
+        },
+        "__rtruediv__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__ge__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___ge__", "int___unbox__"]
+            "requires": ["int___ge__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__gt__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___gt__", "int___unbox__"]
+            "requires": ["int___gt__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__lt__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___lt__", "int___unbox__"]
+            "requires": ["int___lt__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__le__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___le__", "int___unbox__"]
+            "requires": ["int___le__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__pos__": {
             "args": ["float"],
@@ -361,11 +406,12 @@
         "__neg__": {
             "args": ["float"],
             "type": "float",
-            "requires": ["int___neg__", "__prim__perm___box__", "unbox"]
+            "requires": ["int___neg__", "__prim__perm___box__", "unbox", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__int__": {
             "args": ["float"],
-            "type": "int"
+            "type": "int",
+            "requires": ["unbox", "__prim__int___box__", "float___is_nan__", "float___is_inf__"]
         }
     },
     "extends": "object"
diff --git a/src/nagini_translation/translators/contract.py b/src/nagini_translation/translators/contract.py
index 5c77a228..782152d3 100644
--- a/src/nagini_translation/translators/contract.py
+++ b/src/nagini_translation/translators/contract.py
@@ -16,6 +16,7 @@
     GET_OLD_FUNC,
     GLOBAL_VAR_FIELD,
     INT_TYPE,
+    FLOAT_TYPE,
     JOINABLE_FUNC,
     METHOD_ID_DOMAIN,
     PMSET_TYPE,
@@ -985,6 +986,13 @@ def translate_exists(self, node: ast.Call, ctx: Context,
                                    self.to_position(node, ctx),
                                    self.no_info(ctx))
         return dom_stmt, exists
+    
+    def translate_isNaN(self, node: ast.Call, ctx: Context) -> StmtsAndExpr:
+        assert len(node.args) == 1
+        stmt, expr = self.translate_expr(node.args[0], ctx, self.viper.Perm, True)
+        float_class = ctx.module.global_module.classes[FLOAT_TYPE]
+        call = self.get_function_call(float_class, '__isNaN', [expr], [None], node, ctx, self.to_position(node, ctx))
+        return stmt, call
 
     def translate_contractfunc_call(self, node: ast.Call, ctx: Context,
                                     impure=False, statement=False) -> StmtsAndExpr:
@@ -1104,6 +1112,8 @@ def translate_contractfunc_call(self, node: ast.Call, ctx: Context,
             return self.translate_get_arg(node, ctx)
         elif func_name == 'getOld':
             return self.translate_get_old(node, ctx)
+        elif func_name == 'isNaN':
+            return self.translate_isNaN(node, ctx)
         elif func_name == 'getMethod':
             raise InvalidProgramException(node, 'invalid.get.method.use')
         elif func_name == 'arg':
diff --git a/src/nagini_translation/translators/expression.py b/src/nagini_translation/translators/expression.py
index 9fe33eb8..236a520e 100644
--- a/src/nagini_translation/translators/expression.py
+++ b/src/nagini_translation/translators/expression.py
@@ -27,6 +27,7 @@
     RIGHT_OPERATOR_FUNCTIONS,
     PRIMITIVE_INT_TYPE,
     PRIMITIVE_PERM_TYPE,
+    PRIMITIVE_BOOL_TYPE,
     SET_TYPE,
     STRING_TYPE,
     THREAD_DOMAIN,
@@ -68,6 +69,7 @@
 from nagini_translation.translators.abstract import Context
 from nagini_translation.translators.common import CommonTranslator
 from typing import List, Optional, Tuple, Union
+from math import isnan, isinf
 
 
 # Maps function names to bools; caches which functions take an additonal argument
@@ -255,24 +257,25 @@ def translate_Num(self, node: ast.Num, ctx: Context) -> StmtsAndExpr:
     def translate_float_literal(self, lit: float, node: ast.AST, ctx: Context) -> Expr:
         pos = self.to_position(node, ctx)
         info = self.no_info(ctx)
+
+        float_class = ctx.module.global_module.classes[FLOAT_TYPE]
         if ctx.float_encoding == "real":
+            if isnan(lit):
+                return self.get_function_call(float_class, '__box_nan', [], [], node, ctx, pos)
+            if isinf(lit) and lit > 0:
+                return self.get_function_call(float_class, '__box_inf', [self.viper.FalseLit(pos, info)], [None], node, ctx, pos)
+            if isinf(lit) and lit < 0:
+                return self.get_function_call(float_class, '__box_inf', [self.viper.TrueLit(pos, info)], [None], node, ctx, pos)
+
             prim_perm_class = ctx.module.global_module.classes[PRIMITIVE_PERM_TYPE]
-            try:
-                num, den = lit.as_integer_ratio()
-                num_lit = self.viper.IntLit(num, pos, info)
-                den_lit = self.viper.IntLit(den, pos, info)
-                frac = self.viper.FractionalPerm(num_lit, den_lit, pos, info)
-                float_val = self.get_function_call(prim_perm_class, '__box__', [frac],
-                                                   [None], node, ctx, pos)
-                return float_val
-            except ValueError:
-                # NaN
-                raise InvalidProgramException(node, 'non.real.float')
-            except OverflowError:
-                # Inf
-                raise InvalidProgramException(node, 'non.real.float')
+            num, den = lit.as_integer_ratio()
+            num_lit = self.viper.IntLit(num, pos, info)
+            den_lit = self.viper.IntLit(den, pos, info)
+            frac = self.viper.FractionalPerm(num_lit, den_lit, pos, info)
+            float_val = self.get_function_call(prim_perm_class, '__box__', [frac],
+                                               [None], node, ctx, pos)
+            return float_val
         if ctx.float_encoding == "ieee32":
-            float_class = ctx.module.global_module.classes[FLOAT_TYPE]
             import struct
             bytes_val = struct.pack('!f', lit)
             int_val = int.from_bytes(bytes_val, "big")
@@ -283,7 +286,6 @@ def translate_float_literal(self, lit: float, node: ast.AST, ctx: Context) -> Ex
         import logging
         logging.warning("Floating point operations are uninterpreted by default. To use interpreted "
                         "floating point operations, use option --float-encoding")
-        float_class = ctx.module.global_module.classes[FLOAT_TYPE]
         index_lit = self.viper.IntLit(ctx.get_fresh_int(), pos, info)
         float_val = self.get_function_call(float_class, '__create__', [index_lit],
                                            [None], node, ctx, pos)
diff --git a/tests/functional/translation/float_real/test_non_real.py b/tests/functional/translation/float_real/test_non_real.py
index b82088fd..e7234675 100644
--- a/tests/functional/translation/float_real/test_non_real.py
+++ b/tests/functional/translation/float_real/test_non_real.py
@@ -4,7 +4,6 @@
 from nagini_contracts.contracts import *
 
 def specialVals() -> None:
-    #:: ExpectedOutput(invalid.program:non.real.float)
     nan = float("nan")
     nf = float("inF")
     one = float("1.0")
diff --git a/tests/functional/verification/float_real/test_float.py b/tests/functional/verification/float_real/test_float.py
index 9ffcd36a..559c41e4 100644
--- a/tests/functional/verification/float_real/test_float.py
+++ b/tests/functional/verification/float_real/test_float.py
@@ -49,6 +49,7 @@ def sqr3(num : float) -> float:
     return num * num
 
 def arith(num: float) -> float:
+    Requires(not isNaN(num))
     Ensures(Result() == num + 3)
     return num + 1.0 + 2.0
 
diff --git a/tests/functional/verification/float_real/test_special_vals.py b/tests/functional/verification/float_real/test_special_vals.py
new file mode 100644
index 00000000..1e937bf9
--- /dev/null
+++ b/tests/functional/verification/float_real/test_special_vals.py
@@ -0,0 +1,301 @@
+def test_bool() -> None:
+  assert bool(float('nan')) == True
+  assert bool(1.0) == True
+  assert bool(0.0) == False
+  assert bool(-1.0) == True
+  assert bool(float('inf')) == True
+  assert bool(float('-inf')) == True
+
+  #:: ExpectedOutput(assert.failed:assertion.false)
+  assert False
+
+def test_nan_float_compare() -> None:
+  assert (float('nan') >= 1.0) == False
+  assert (float('nan') >= 0.0) == False
+  assert (float('nan') >= -1.0) == False
+  assert (1.0 >= float('nan')) == False
+  assert (0.0 >= float('nan')) == False
+  assert (-1.0 >= float('nan')) == False
+  assert (float('nan') >= float('nan')) == False
+  
+  assert (float('nan') > 1.0) == False
+  assert (float('nan') > 0.0) == False
+  assert (float('nan') > -1.0) == False
+  assert (1.0 > float('nan')) == False
+  assert (0.0 > float('nan')) == False
+  assert (-1.0 > float('nan')) == False
+  assert (float('nan') > float('nan')) == False
+  
+  assert (float('nan') <= 1.0) == False
+  assert (float('nan') <= 0.0) == False
+  assert (float('nan') <= -1.0) == False
+  assert (1.0 <= float('nan')) == False
+  assert (0.0 <= float('nan')) == False
+  assert (-1.0 <= float('nan')) == False
+  assert (float('nan') <= float('nan')) == False
+  
+  assert (float('nan') < 1.0) == False
+  assert (float('nan') < 0.0) == False
+  assert (float('nan') < -1.0) == False
+  assert (1.0 < float('nan')) == False
+  assert (0.0 < float('nan')) == False
+  assert (-1.0 < float('nan')) == False
+  assert (float('nan') < float('nan')) == False
+  
+  assert (float('nan') == 1.0) == False
+  assert (float('nan') == 0.0) == False
+  assert (float('nan') == -1.0) == False
+  assert (1.0 ==  float('nan')) == False
+  assert (0.0 ==  float('nan')) == False
+  assert (-1.0 == float('nan')) == False
+  assert (float('nan') == float('nan')) == False
+
+  #:: ExpectedOutput(assert.failed:assertion.false)
+  assert False
+
+
+
+def test_nan_int_compare() -> None:
+  assert (float('nan') >= 1) == False
+  assert (float('nan') >= 0) == False
+  assert (float('nan') >= -1) == False
+  assert (1 >= float('nan')) == False
+  assert (0 >= float('nan')) == False
+  assert (-1 >= float('nan')) == False
+  
+  assert (float('nan') > 1) == False
+  assert (float('nan') > 0) == False
+  assert (float('nan') > -1) == False
+  assert (1 > float('nan')) == False
+  assert (0 > float('nan')) == False
+  assert (-1 > float('nan')) == False
+  
+  assert (float('nan') <= 1) == False
+  assert (float('nan') <= 0) == False
+  assert (float('nan') <= -1) == False
+  assert (1 <= float('nan')) == False
+  assert (0 <= float('nan')) == False
+  assert (-1 <= float('nan')) == False
+  
+  assert (float('nan') < 1) == False
+  assert (float('nan') < 0) == False
+  assert (float('nan') < -1) == False
+  assert (1 < float('nan')) == False
+  assert (0 < float('nan')) == False
+  assert (-1 < float('nan')) == False
+  
+  assert (float('nan') == 1) == False
+  assert (float('nan') == 0) == False
+  assert (float('nan') == -1) == False
+  assert (1 ==  float('nan')) == False
+  assert (0 ==  float('nan')) == False
+  assert (-1 == float('nan')) == False
+
+  #:: ExpectedOutput(assert.failed:assertion.false)
+  assert False
+
+def test_inf_compare() -> None:
+  assert (float('inf') > float('inf')) == False
+  assert (float('inf') > 0.0) == True
+  assert (float('inf') > 0) == True
+  assert (float('inf') > float('-inf')) == True
+  
+  assert (float('inf') >= float('inf')) == True
+  assert (float('inf') >= 0.0) == True
+  assert (float('inf') >= 0) == True
+  assert (float('inf') >= float('-inf')) == True
+  
+  assert (float('inf') < float('inf')) == False
+  assert (float('inf') < 0.0) == False
+  assert (float('inf') < 0) == False
+  assert (float('inf') < float('-inf')) == False
+  
+  assert (float('inf') <= float('inf')) == True
+  assert (float('inf') <= 0.0) == False
+  assert (float('inf') < 0) == False
+  assert (float('inf') <= float('-inf')) == False
+  
+  assert (float('inf') == float('inf')) == True
+  assert (float('inf') == 0.0) == False
+  assert (float('inf') == 0) == False
+  assert (float('inf') == float('-inf')) == False
+
+  #:: ExpectedOutput(assert.failed:assertion.false)
+  assert False
+  
+def test_neg_inf_compare() -> None:
+  assert (float('-inf') > float('inf')) == False
+  assert (float('-inf') > 0.0) == False
+  assert (float('-inf') > 0) == False
+  assert (float('-inf') > float('-inf')) == False
+  
+  assert (float('-inf') >= float('inf')) == False
+  assert (float('-inf') >= 0.0) == False
+  assert (float('-inf') >= 0) == False
+  assert (float('-inf') >= float('-inf')) == True
+  
+  assert (float('-inf') < float('inf')) == True
+  assert (float('-inf') < 0.0) == True
+  assert (float('-inf') < 0) == True
+  assert (float('-inf') < float('-inf')) == False
+  
+  assert (float('-inf') <= float('inf')) == True
+  assert (float('-inf') <= 0.0) == True
+  assert (float('-inf') <= 0) == True
+  assert (float('-inf') <= float('-inf')) == True
+  
+  assert (float('-inf') == float('inf')) == False
+  assert (float('-inf') == 0.0) == False
+  assert (float('-inf') == 0) == False
+  assert (float('-inf') == float('-inf')) == True
+
+  #:: ExpectedOutput(assert.failed:assertion.false)
+  assert False
+
+def test_add() -> None:
+  inf = float('inf')
+  ninf = float('-inf')
+  assert 1.2 + 1.3 == 2.5
+  assert 1.0 + inf == inf
+  assert inf + 1.0 == inf
+  assert ninf + 1.0 == ninf
+  assert 1.0 + ninf == ninf
+  assert inf + inf == inf
+  assert ninf + ninf == ninf
+  assert inf + ninf is float('nan')
+  assert ninf + inf is float('nan')
+  assert inf + float('nan') is float('nan')
+  assert float('nan') + inf is float('nan')
+  assert ninf + float('nan') is float('nan')
+  assert float('nan') + ninf is float('nan')
+  assert float('nan') + 1.0 is float('nan')
+  assert 1.0 + float('nan') is float('nan')
+  assert float('nan') + float('nan') is float('nan')
+
+  assert 1 + 1.5 == 2.5
+  assert 1 + inf == inf
+  assert inf + 1 == inf
+  assert ninf + 1 == ninf
+  assert 1 + ninf == ninf
+  assert float('nan') + 1 is float('nan')
+  assert 1 + float('nan') is float('nan')
+
+  #:: ExpectedOutput(assert.failed:assertion.false)
+  assert False
+
+def test_subtract() -> None:
+  inf = float('inf')
+  ninf = float('-inf')
+  assert 2.0 - 0.5 == 1.5
+  assert 1.0 - inf == ninf
+  assert inf - 1.0 == inf
+  assert ninf - 1.0 == ninf
+  assert 1.0 - ninf == inf
+  assert inf - inf is float('nan')
+  assert ninf - ninf is float('nan')
+  assert inf - ninf == inf
+  assert ninf - inf == ninf
+  assert inf - float('nan') is float('nan')
+  assert float('nan') - inf is float('nan')
+  assert ninf - float('nan') is float('nan')
+  assert float('nan') - ninf is float('nan')
+  assert float('nan') - 1.0 is float('nan')
+  assert 1.0 - float('nan') is float('nan')
+  assert float('nan') - float('nan') is float('nan')
+
+  assert 1 - 1.5 == -0.5
+  assert 1 - inf == ninf
+  assert inf - 1 == inf
+  assert ninf - 1 == ninf
+  assert 1 - ninf == inf
+  assert float('nan') - 1 is float('nan')
+  assert 1 - float('nan') is float('nan')
+
+  #:: ExpectedOutput(assert.failed:assertion.false)
+  assert False
+
+def test_multiply() -> None:
+  inf = float('inf')
+  ninf = float('-inf')
+  assert 1.5 * -2.0 == -3
+  assert 1.0 * inf == inf
+  assert inf * 1.0 == inf
+  assert -1.0 * inf == ninf
+  assert inf * -1.0 == ninf
+  assert ninf * 1.0 == ninf
+  assert 1.0 * ninf == ninf
+  assert -1.0 * ninf == inf
+  assert ninf * -1.0 == inf
+  assert 0.0 * inf is float('nan')
+  assert inf * 0.0 is float('nan')
+  assert 0.0 * ninf is float('nan')
+  assert ninf * 0.0 is float('nan')
+  assert inf * inf == inf
+  assert ninf * ninf == inf
+  assert inf * ninf == ninf
+  assert ninf * inf == ninf
+  assert inf * float('nan') is float('nan')
+  assert float('nan') * inf is float('nan')
+  assert ninf * float('nan') is float('nan')
+  assert float('nan') * ninf is float('nan')
+  assert float('nan') * 1.0 is float('nan')
+  assert 1.0 * float('nan') is float('nan')
+  assert float('nan') * float('nan') is float('nan')
+
+  assert 1 * -2.0 == -2
+  assert 1 * inf == inf
+  assert inf * 1 == inf
+  assert -1 * inf == ninf
+  assert inf * -1 == ninf
+  assert ninf * 1 == ninf
+  assert 1 * ninf == ninf
+  assert -1 * ninf == inf
+  assert ninf * -1 == inf
+  assert 0 * inf is float('nan')
+  assert inf * 0 is float('nan')
+  assert 0 * ninf is float('nan')
+  assert ninf * 0 is float('nan')
+  assert float('nan') * 1 is float('nan')
+  assert 1 * float('nan') is float('nan')
+
+  #:: ExpectedOutput(assert.failed:assertion.false)
+  assert False
+
+def test_divide() -> None:
+  inf = float('inf')
+  ninf = float('-inf')
+  assert 2.5 / 5.0 == 0.5
+  assert 1.0 / inf == 0.0
+  assert inf / 1.0 == inf
+  assert -1.0 / inf == 0.0
+  assert inf / -1.0 == ninf
+  assert ninf / 1.0 == ninf
+  assert 1.0 / ninf == 0.0
+  assert ninf / -1.0 == inf
+  assert -1.0 / ninf == 0.0
+  assert inf / inf is float('nan')
+  assert ninf / ninf is float('nan')
+  assert inf / ninf is float('nan')
+  assert ninf / inf is float('nan')
+  assert inf / float('nan') is float('nan')
+  assert float('nan') / inf is float('nan')
+  assert ninf / float('nan') is float('nan')
+  assert float('nan') / ninf is float('nan')
+  assert float('nan') / 1.0 is float('nan')
+  assert 1.0 / float('nan') is float('nan')
+  assert float('nan') / float('nan') is float('nan')
+
+  assert 2.5 / 5 == 0.5
+  assert 1 / inf == 0
+  assert inf / 1 == inf
+  assert -1 / inf == 0
+  assert inf / -1 == ninf
+  assert ninf / 1 == ninf
+  assert 1 / ninf == 0
+  assert ninf / -1 == inf
+  assert -1 / ninf == 0
+  assert float('nan') / 1 is float('nan')
+  assert 1 / float('nan') is float('nan')
+
+  #:: ExpectedOutput(assert.failed:assertion.false)
+  assert False
\ No newline at end of file