Fix real float test cases failing due to rounding errors

marcoeilers · May 21, 2024 · c85418b · c85418b
1 parent 6ae6912
commit c85418b
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 9 deletions.
diff --git a/src/nagini_translation/resources/float_real.sil b/src/nagini_translation/resources/float_real.sil
@@ -181,10 +181,10 @@ function float___sub__(self: Ref, other: Ref): Ref
     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  ||
+    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 ||
+    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 &&
@@ -202,10 +202,10 @@ function float___rsub__(self: Ref, other: Ref): Ref
     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  ||
+    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 ||
+    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 &&

diff --git a/tests/functional/verification/float_real/test_special_vals.py b/tests/functional/verification/float_real/test_special_vals.py
@@ -172,7 +172,7 @@ def test_add() -> None:
   assert 1.0 + float('nan') is float('nan')
   assert float('nan') + float('nan') is float('nan')
 
-  assert 1 + 1.3 == 2.3
+  assert 1 + 1.5 == 2.5
   assert 1 + inf == inf
   assert inf + 1 == inf
   assert ninf + 1 == ninf
@@ -186,7 +186,7 @@ def test_add() -> None:
 def test_subtract() -> None:
   inf = float('inf')
   ninf = float('-inf')
-  assert 2.0 - 0.6 == 1.4
+  assert 2.0 - 0.5 == 1.5
   assert 1.0 - inf == ninf
   assert inf - 1.0 == inf
   assert ninf - 1.0 == ninf
@@ -203,7 +203,7 @@ def test_subtract() -> None:
   assert 1.0 - float('nan') is float('nan')
   assert float('nan') - float('nan') is float('nan')
 
-  assert 1 - 1.2 == -0.2
+  assert 1 - 1.5 == -0.5
   assert 1 - inf == ninf
   assert inf - 1 == inf
   assert ninf - 1 == ninf
@@ -217,7 +217,7 @@ def test_subtract() -> None:
 def test_multiply() -> None:
   inf = float('inf')
   ninf = float('-inf')
-  assert 1.2 * -1.3 == -1.56
+  assert 1.5 * -2.0 == -3
   assert 1.0 * inf == inf
   assert inf * 1.0 == inf
   assert -1.0 * inf == ninf
@@ -242,7 +242,7 @@ def test_multiply() -> None:
   assert 1.0 * float('nan') is float('nan')
   assert float('nan') * float('nan') is float('nan')
 
-  assert 1.2 * -1.3 == -1.56
+  assert 1 * -2.0 == -2
   assert 1 * inf == inf
   assert inf * 1 == inf
   assert -1 * inf == ninf