diff --git a/src/plugins/wp/tests/wp_acsl/bitwise.i b/src/plugins/wp/tests/wp_acsl/bitwise.i
index d9dcf8fe5032cfc5f5dd6bac7718062744947fde..b2e5594f27096dbe8e31f400e04a8cc75ee1abce 100644
--- a/src/plugins/wp/tests/wp_acsl/bitwise.i
+++ b/src/plugins/wp/tests/wp_acsl/bitwise.i
@@ -124,3 +124,9 @@ void lemma(unsigned a, unsigned b, unsigned k) {
   //@ check           ( a & b & 77 & ((1 << (k & 55))-1) ) == ( (a & b & 77) % (1 << (k & 55)) );
 
 }
+
+//@ ensures \result == (x & 0xFF) ;
+unsigned char cast_uchar(int x) {
+  unsigned char c = x;
+  return c;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
index 351c09e561f43e8aad7bbdf65157ecc656389eae..232b2653404ec97a49e685a92afecc0955b00594 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
@@ -218,6 +218,14 @@ Assume {
 }
 Prove: b != a.
 
+------------------------------------------------------------
+------------------------------------------------------------
+  Function cast_uchar
+------------------------------------------------------------
+
+Goal Post-condition (file bitwise.i, line 128) in 'cast_uchar':
+Prove: true.
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function lemma
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
index 946e96312f88b058955d3537a07162b6c37de557..413c2326caae6ae63dcdeaa67818f7b7376c90ad 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
@@ -2,7 +2,7 @@
 [kernel] Parsing bitwise.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 37 goals scheduled
+[wp] 38 goals scheduled
 [wp] [Qed] Goal typed_band_ensures : Valid
 [wp] [Qed] Goal typed_band_ensures_band0 : Valid
 [wp] [Qed] Goal typed_band_bit0_ensures_band1 : Valid
@@ -40,8 +40,9 @@
 [wp] [Qed] Goal typed_lemma_check_5 : Valid
 [wp] [Qed] Goal typed_lemma_check_6 : Valid
 [wp] [Qed] Goal typed_lemma_check_7 : Valid
-[wp] Proved goals:   37 / 37
-  Qed:            33 
+[wp] [Qed] Goal typed_cast_uchar_ensures : Valid
+[wp] Proved goals:   38 / 38
+  Qed:            34 
   Alt-Ergo:        4
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
@@ -55,4 +56,5 @@
   band_bool                 1        1        2       100%
   bxor_bool                 1        1        2       100%
   lemma                     7        -        7       100%
+  cast_uchar                1        -        1       100%
 ------------------------------------------------------------