diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle
index 39e9f3d83596b5d28e157b5556f5c0450b7badb0..7925fe574f94b73f177e4cb58eda070ae382061b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle
@@ -15,10 +15,10 @@ Assume {
   If x < ((1.0/100000) + y)
   Then {
     If y < ((1.0/100000) + x)
-    Then { (* Return *) Have: dequal_0 = 1. }
-    Else { (* Return *) Have: dequal_0 = 0. }
+    Then { Have: dequal_0 = 1. }
+    Else { Have: dequal_0 = 0. }
   }
-  Else { (* Return *) Have: dequal_0 = 0. }
+  Else { Have: dequal_0 = 0. }
 }
 Prove: (abs_real(x - y) < (1.0/100000)) <-> (dequal_0 != 0).
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
index acae1296cda548c49122e49e55befe3e44cd1d16..fcf6b16825571012a6242700f16831786af9bcda 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
@@ -17,10 +17,10 @@ Assume {
   Then {
     If lt_f64(to_f64((-5902958103587057.0/590295810358705651712)),
          sub_f64(x, y))
-    Then { (* Return *) Have: dequal_0 = 1. }
-    Else { (* Return *) Have: dequal_0 = 0. }
+    Then { Have: dequal_0 = 1. }
+    Else { Have: dequal_0 = 0. }
   }
-  Else { (* Return *) Have: dequal_0 = 0. }
+  Else { Have: dequal_0 = 0. }
 }
 Prove: (abs_real(of_f64(x) - of_f64(y)) < (1.0/100000)) <-> (dequal_0 != 0).
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
index 0697c55a730d66e76ef9f11d90bfc7c1664240ff..f921ae4ce125d33e1ffdf74c9a30509986096d67 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
@@ -34,10 +34,9 @@ Assume {
     Have: i_1 = i.
     (* Then *)
     Have: Mint_0[shift_sint32(q, j)] <= x.
-    (* Return *)
     Have: diag_0 = 0.
   }
-  Else { (* Return *) Have: diag_0 = 1. }
+  Else { Have: diag_0 = 1. }
 }
 Prove: (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < n) ->
         (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < m) ->