diff --git a/src/plugins/wp/tests/wp_acsl/boolean.i b/src/plugins/wp/tests/wp_acsl/boolean.i
new file mode 100644
index 0000000000000000000000000000000000000000..212b2117f669cca2fdc7d4ab0756fba5f8babeaa
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/boolean.i
@@ -0,0 +1,16 @@
+/* run.config
+OPT: -wp-prover alt-ergo -wp-gen
+*/
+ /*@
+        logic boolean u8_continue_f(unsigned char b) =
+          0x80<=b && 0xC0 > b;
+    */
+
+    /*@
+        assigns \nothing;
+        ensures  u8_continue_f(b) == \result==1;
+    */
+    int u8_is_continue(const unsigned char b)
+    {
+        return b >= 0x80 && b <= 0xBF;
+    }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0ae8f9eabef4b6269b768c7ffc0a0e47d608d60a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
@@ -0,0 +1,50 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/boolean.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 4 goals scheduled
+[wp] [Qed] Goal typed_u8_is_continue_assigns_part3 : Valid
+[wp] [Qed] Goal typed_u8_is_continue_assigns_part2 : Valid
+[wp] [Qed] Goal typed_u8_is_continue_assigns_part1 : Valid
+[wp] 4 goals generated
+------------------------------------------------------------
+  Function u8_is_continue
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/boolean.i, line 11) in 'u8_is_continue':
+Assume {
+  Type: is_uint8(b) /\ is_sint32(u8_is_continue_0).
+  If 128 <= b
+  Then {
+    If b <= 191
+    Then { Have: u8_is_continue_0 = 1. }
+    Else { Have: u8_is_continue_0 = 0. }
+  }
+  Else { Have: u8_is_continue_0 = 0. }
+}
+Prove: (u8_is_continue_0 = 1) /\
+    ((L_u8_continue_f(b)=true) <-> (u8_is_continue_0 != 0)).
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'u8_is_continue' (1/3):
+Effect at line 15
+Prove: true.
+Prover Qed returns Valid
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'u8_is_continue' (2/3):
+Effect at line 15
+Prove: true.
+Prover Qed returns Valid
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'u8_is_continue' (3/3):
+Effect at line 15
+Prove: true.
+Prover Qed returns Valid
+
+------------------------------------------------------------