diff --git a/src/plugins/aorai/tests/ya/aorai_ptr_field.i b/src/plugins/aorai/tests/ya/aorai_ptr_field.i
index 9f1316be55c1e7c25305f22bdbed66a594434bb9..24c8ffc30a7231b26a8e6febc12d553b1c2a39f3 100644
--- a/src/plugins/aorai/tests/ya/aorai_ptr_field.i
+++ b/src/plugins/aorai/tests/ya/aorai_ptr_field.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 struct S { int x; };
diff --git a/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle b/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle
index b9750505021bd05f5fc1a55c85159b8c653a0ff2..d8cb4fbaee53d3fb52af093090ef0d12c43002b7 100644
--- a/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/aorai_ptr_field.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_aorai_ptr_field_0.i (no preprocessing)
 /* Generated by Frama-C */
 struct S {
@@ -12,8 +11,8 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int S0 = 1; */
 /*@ ghost int S1 = 0; */
 /*@ ghost
@@ -38,6 +37,7 @@ enum aorai_OpStatusList {
   {
     int S0_tmp;
     int S1_tmp;
+    /@ slevel full; @/
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     S0_tmp = S0;
@@ -73,6 +73,7 @@ enum aorai_OpStatusList {
   {
     int S0_tmp;
     int S1_tmp;
+    /@ slevel full; @/
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle
index 5d9a38bc1e4b760ac98152b2e6c6958812759e8d..45a91772ac37c0a8a776a8b3f720ea67c19b56ee 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/aorai_ptr_field.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_aorai_ptr_field_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/serial.ya b/src/plugins/aorai/tests/ya/serial.ya
index 8fde0de6e29e464e59cb682577826d94731f31fc..9f995d7f19fd7ec4389f2f97da0cb3b52d03d553 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 : { 0 } -> Error;
+Error : { false } -> Error;
 
 Wait1 :
   { CALL(input_status) } -> StatusReq1
@@ -129,25 +129,25 @@ DataReq1 :
 DataReq2 :
   { input_data().\result & 192 == 128 } -> Wait2
 | { input_data().\result & 192 == 192 } -> Wait1
-| { input_data().\result & 128 == 0 } $x1 := \result -> Wait3
+| { input_data().\result & 128 == 0 } $x1 := \result; -> Wait3
 ;
 
 DataReq3 :
   { input_data().\result & 192 == 128 } -> Wait2
 | { input_data().\result & 192 == 192 } -> Wait1
-| { input_data().\result & 128 == 0 } $x2 := \result -> Wait4
+| { input_data().\result & 128 == 0 } $x2 := \result; -> Wait4
 ;
 
 DataReq4 :
   { input_data().\result & 192 == 128 } -> Wait2
 | { input_data().\result & 192 == 192 } -> Wait1
-| { input_data().\result & 128 == 0 } $y1 := \result -> Wait5
+| { input_data().\result & 128 == 0 } $y1 := \result; -> Wait5
 ;
 
 DataReq5 :
   { input_data().\result & 192 == 128 } -> Wait2
 | { input_data().\result & 192 == 192 } -> Wait1
-| { input_data().\result & 128 == 0 } $y2 := \result -> Complete
+| { input_data().\result & 128 == 0 } $y2 := \result; -> Complete
 ;
 
 Complete :