diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
index a9b85468c5385d78c9e88f4ee6bae6836c264e57..23c84d0e8990c2208a39ddf037d973f0439e796d 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,13 +1,9 @@
 [kernel] Parsing tests/ya/serial.c (with preprocessing)
-[aorai] tests/ya/serial.c:79: Warning: 
-  Call to output not conforming to automaton (post-cond). Assuming it is on a dead path
-[aorai] tests/ya/serial.c:25: Warning: 
-  Call to output not conforming to automaton (pre-cond). Assuming it is on a dead path
 [kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
-[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:98: Warning: 
+[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:1359: Warning: 
   Calling undeclared function Frama_C_interval. Old style K&R code?
-[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:125: Warning: 
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:851: Warning: 
   Neither code nor specification for function Frama_C_interval, generating default assigns from the prototype
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:125: Warning: 
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:851: Warning: 
   Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
index 7073942e7e1c130d4fd0b6aa6a4df75d5bf2e332..3bf7ab6cfac3dd7486a1b3460d892aa758204eff 100644
--- a/src/plugins/aorai/tests/ya/serial.c
+++ b/src/plugins/aorai/tests/ya/serial.c
@@ -2,11 +2,21 @@
   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256
 */
 /* run.config_prove
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance @PROVE_OPTIONS@
+OPT: -cpp-extra-args="-DFOR_WP" -aorai-automata @PTEST_DIR@/@PTEST_NAME@_wp.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance @PROVE_OPTIONS@
 */
 
 #include "__fc_builtin.h"
 
+#ifndef FOR_WP
+#define BW_AND &
+#define BW_AND2 &
+#define BW_AND3 &
+#else
+#define BW_AND ==
+#define BW_AND2 >=
+#define BW_AND3 <=
+#endif
+
 /*@ assigns \result \from \nothing;
     ensures 0 <= \result < 0x100; */
 int input_status(void) {
@@ -29,8 +39,8 @@ int read(int *status)
 {
   int s = input_status();
 
-  if (s & 0x01) {
-    *status = s & 0x0e;
+  if (s BW_AND2 0x01) {
+    *status = s BW_AND 0x0e;
     return input_data();
   }
 
@@ -56,7 +66,7 @@ void main(void)
         n = 0;
         continue;
       }
-      if (data & 0x80) { // status received
+      if (data BW_AND3 0x80) { // status received
         if (n != 0) { // but data was expected
           n = 0;
           continue;
@@ -72,7 +82,7 @@ void main(void)
       buffer[n++] = data;
 
       if (n == 5) { // the packet is completely read
-        if ((buffer[0] & 0x40) == 0) // it is a release action
+        if ((buffer[0] BW_AND 0x40) == 0) // it is a release action
         {
           int x = buffer[1] + 0x80 * buffer[2];
           int y = buffer[3] + 0x80 * buffer[4];
diff --git a/src/plugins/aorai/tests/ya/serial.ya b/src/plugins/aorai/tests/ya/serial.ya
index 9f995d7f19fd7ec4389f2f97da0cb3b52d03d553..fed4f5cf370a63966d1def03be121ebdfafeaa4a 100644
--- a/src/plugins/aorai/tests/ya/serial.ya
+++ b/src/plugins/aorai/tests/ya/serial.ya
@@ -7,7 +7,7 @@ $x2 : int;
 $y1 : int;
 $y2 : int;
 
-Error : { false } -> Error;
+Error : { true } -> Error;
 
 Wait1 :
   { CALL(input_status) } -> StatusReq1
diff --git a/src/plugins/aorai/tests/ya/serial_wp.ya b/src/plugins/aorai/tests/ya/serial_wp.ya
new file mode 100644
index 0000000000000000000000000000000000000000..a796279cdbd6b29f51504950f8ae0cafa758e2bf
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/serial_wp.ya
@@ -0,0 +1,159 @@
+%init : Wait1;
+%deterministic;
+%observables: input_status, input_data, output;
+
+$x1 : int;
+$x2 : int;
+$y1 : int;
+$y2 : int;
+
+Error : { true } -> Error;
+
+Wait1 :
+  { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait1
+;
+
+Wait2 :
+  { CALL(input_status) } -> StatusReq2
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait2
+;
+
+Wait3 :
+  { CALL(input_status) } -> StatusReq3
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait3
+;
+
+Wait4 :
+  { CALL(input_status) } -> StatusReq4
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait4
+;
+
+Wait5 :
+  { CALL(input_status) } -> StatusReq5
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait5
+;
+
+StatusReq1 :
+  { input_status().\result < 1 } -> Wait1
+| { input_status().\result == 14 } -> StatusOk1
+| other -> StatusError
+;
+
+StatusReq2 :
+  { input_status().\result < 1 } -> Wait2
+| { input_status().\result == 14 } -> StatusOk2
+| other -> StatusError
+;
+
+StatusReq3 :
+  { input_status().\result < 1 } -> Wait3
+| { input_status().\result == 14 } -> StatusOk3
+| other -> StatusError
+;
+
+StatusReq4 :
+  { input_status().\result < 1 } -> Wait4
+| { input_status().\result == 14 } -> StatusOk4
+| other -> StatusError
+;
+
+StatusReq5 :
+  { input_status().\result < 1 } -> Wait5
+| { input_status().\result == 14 } -> StatusOk5
+| other -> StatusError
+;
+
+StatusError :
+  { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> DataReqE
+| { CALL(output) } -> Error
+| other -> StatusError
+;
+
+StatusOk1 :
+  { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> DataReq1
+| { CALL(output) } -> Error
+| other -> StatusOk1
+;
+
+StatusOk2 :
+  { CALL(input_status) } -> StatusReq2
+| { CALL(input_data) } -> DataReq2
+| { CALL(output) } -> Error
+| other -> StatusOk2
+;
+
+StatusOk3 :
+  { CALL(input_status) } -> StatusReq3
+| { CALL(input_data) } -> DataReq3
+| { CALL(output) } -> Error
+| other -> StatusOk3
+;
+
+StatusOk4 :
+  { CALL(input_status) } -> StatusReq4
+| { CALL(input_data) } -> DataReq4
+| { CALL(output) } -> Error
+| other -> StatusOk4
+;
+
+StatusOk5 :
+  { CALL(input_status) } -> StatusReq5
+| { CALL(input_data) } -> DataReq5
+| { CALL(output) } -> Error
+| other -> StatusOk5
+;
+
+DataReqE :
+  { RETURN(input_data) } -> Wait1
+;
+
+DataReq1 :
+  { input_data().\result <= 128 && input_data().\result != 64 } -> Wait2
+| { input_data().\result == 64 } -> Wait1
+| { input_data().\result > 128 } -> Wait1
+;
+
+DataReq2 :
+  { input_data().\result <= 128 && input_data().\result != 64 } -> Wait2
+| { input_data().\result == 64 } -> Wait1
+| { input_data().\result > 128 } $x1 := \result; -> Wait3
+;
+
+DataReq3 :
+  { input_data().\result <= 128 && input_data().\result != 64 } -> Wait2
+| { input_data().\result == 64 } -> Wait1
+| { input_data().\result > 128 } $x2 := \result; -> Wait4
+;
+
+DataReq4 :
+  { input_data().\result <= 128 && input_data().\result != 64 } -> Wait2
+| { input_data().\result == 64 } -> Wait1
+| { input_data().\result > 128 } $y1 := \result; -> Wait5
+;
+
+DataReq5 :
+  { input_data().\result <= 128 && input_data().\result != 64 } -> Wait2
+| { input_data().\result == 64 } -> Wait1
+| { input_data().\result > 128 } $y2 := \result; -> Complete
+;
+
+Complete :
+  { CALL(output) && output().x == $x1 + 128 * $x2 && output().y == $y1 + 128 * $y2 } -> Wait1
+| { CALL(output) && (output().x != $x1 + 128 * $x2 || output().y != $y1 + 128 * $y2) } -> Error
+| { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> Error
+| other -> Complete
+;