diff --git a/src/plugins/wp/tests/wp_acsl/boolean.i b/src/plugins/wp/tests/wp_acsl/boolean.i
index 9e9a3e273d371215fd33aaec8caa8bdd700246b2..2e4b06eda93deec0e268506541ae44afd9509e08 100644
--- a/src/plugins/wp/tests/wp_acsl/boolean.i
+++ b/src/plugins/wp/tests/wp_acsl/boolean.i
@@ -1,6 +1,7 @@
 /* run.config
-DONTRUN: only usable in qualif config
+OPT: -wp-gen -wp-prover why3
 */
+
  /*@
         logic boolean u8_continue_f(unsigned char b) =
           0x80<=b && 0xC0 > b;
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
index 0ae8f9eabef4b6269b768c7ffc0a0e47d608d60a..ea971496a84eeef7fce6ea5c19ceae7878256dec 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
@@ -12,7 +12,7 @@
   Function u8_is_continue
 ------------------------------------------------------------
 
-Goal Post-condition (file tests/wp_acsl/boolean.i, line 11) in 'u8_is_continue':
+Goal Post-condition (file tests/wp_acsl/boolean.i, line 12) in 'u8_is_continue':
 Assume {
   Type: is_uint8(b) /\ is_sint32(u8_is_continue_0).
   If 128 <= b
@@ -23,27 +23,26 @@ Assume {
   }
   Else { Have: u8_is_continue_0 = 0. }
 }
-Prove: (u8_is_continue_0 = 1) /\
-    ((L_u8_continue_f(b)=true) <-> (u8_is_continue_0 != 0)).
+Prove: (L_u8_continue_f(b)=true) <-> (u8_is_continue_0 != 0).
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'u8_is_continue' (1/3):
-Effect at line 15
+Effect at line 16
 Prove: true.
 Prover Qed returns Valid
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'u8_is_continue' (2/3):
-Effect at line 15
+Effect at line 16
 Prove: true.
 Prover Qed returns Valid
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'u8_is_continue' (3/3):
-Effect at line 15
+Effect at line 16
 Prove: true.
 Prover Qed returns Valid