[tests] update Aorai oracles

src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle

@@ -18,15 +18,15 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ lemma in_main_deterministic_trans{L}: \true;
+/*@ check lemma in_main_deterministic_trans{L}: \true;
  */
-/*@ lemma Sf_deterministic_trans{L}: \true;
+/*@ check lemma Sf_deterministic_trans{L}: \true;
  */
-/*@ lemma S_in_f_deterministic_trans{L}: \true;
+/*@ check lemma S_in_f_deterministic_trans{L}: \true;
  */
-/*@ lemma S2_deterministic_trans{L}: \true;
+/*@ check lemma S2_deterministic_trans{L}: \true;
  */
-/*@ lemma S1_deterministic_trans{L}: \true;
+/*@ check lemma S1_deterministic_trans{L}: \true;
  */
 int X;
 /*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */

src/plugins/aorai/tests/aorai/oracle/declared_function.res.oracle

@@ -19,7 +19,7 @@ int f(void);
 /*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
 /*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
 /*@
-lemma I_deterministic_trans{L}:
+check lemma I_deterministic_trans{L}:
   (∀ int __retres_f;
      ¬(\at(aorai_CurOperation,L) ≡ op_f ∧
         \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧

src/plugins/aorai/tests/aorai/oracle/deterministic.res.oracle

@@ -23,22 +23,22 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ lemma Si_deterministic_trans{L}: \true;
+/*@ check lemma Si_deterministic_trans{L}: \true;
  */
-/*@ lemma Sf_deterministic_trans{L}: \true;
+/*@ check lemma Sf_deterministic_trans{L}: \true;
  */
-/*@ lemma S5_deterministic_trans{L}: \true;
+/*@ check lemma S5_deterministic_trans{L}: \true;
  */
-/*@ lemma S4_deterministic_trans{L}: \true;
+/*@ check lemma S4_deterministic_trans{L}: \true;
  */
-/*@ lemma S2_deterministic_trans{L}: \true;
+/*@ check lemma S2_deterministic_trans{L}: \true;
  */
 int X;
 int Y;
 /*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
 /*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
 /*@
-lemma S3_deterministic_trans{L}:
+check lemma S3_deterministic_trans{L}:
   ∀ int x;
     ¬(\at(aorai_CurOperation,L) ≡ op_g ∧
        \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≡ 5 ∧
@@ -46,7 +46,7 @@ lemma S3_deterministic_trans{L}:
        \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≡ 4);
  */
 /*@
-lemma S1_deterministic_trans{L}:
+check lemma S1_deterministic_trans{L}:
   ∀ int __retres_f, int x;
     ¬(\at(aorai_CurOperation,L) ≡ op_f ∧
        \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧ __retres_f ≡ 0 ∧
@@ -54,7 +54,7 @@ lemma S1_deterministic_trans{L}:
        \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≡ 4);
  */
 /*@
-lemma S0_deterministic_trans{L}:
+check lemma S0_deterministic_trans{L}:
   ∀ int c;
     ¬(\at(aorai_CurOperation,L) ≡ op_real_main ∧
        \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ c ≢ 0 ∧

src/plugins/aorai/tests/aorai/oracle/formals.res.oracle

@@ -22,16 +22,16 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ lemma init_deterministic_trans{L}: \true;
+/*@ check lemma init_deterministic_trans{L}: \true;
  */
-/*@ lemma aorai_reject_deterministic_trans{L}: \true;
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
  */
-/*@ lemma OK_deterministic_trans{L}: \true;
+/*@ check lemma OK_deterministic_trans{L}: \true;
  */
 /*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
 /*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
 /*@
-lemma main_0_deterministic_trans{L}:
+check lemma main_0_deterministic_trans{L}:
   ∀ int x;
     ¬(\at(aorai_CurOperation,L) ≡ op_f ∧
        \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≡ 3 ∧
@@ -39,7 +39,7 @@ lemma main_0_deterministic_trans{L}:
        \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≡ 1);
  */
 /*@
-lemma aorai_intermediate_state_0_deterministic_trans{L}:
+check lemma aorai_intermediate_state_0_deterministic_trans{L}:
   ¬(\at(aorai_CurOperation,L) ≡ op_g ∧
      \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
      ¬(\at(aorai_CurOperation,L) ≡ op_g ∧
@@ -48,7 +48,7 @@ lemma aorai_intermediate_state_0_deterministic_trans{L}:
 /*@ ghost int aorai_CurStates = init; */
 /*@ ghost int aorai_x_0 = 0; */
 /*@
-lemma aorai_intermediate_state_2_deterministic_trans{L}:
+check lemma aorai_intermediate_state_2_deterministic_trans{L}:
   ¬(\at(aorai_CurOperation,L) ≡ op_f ∧
      \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
      \at(aorai_x_0,L) ≡ 3 ∧
@@ -58,7 +58,7 @@ lemma aorai_intermediate_state_2_deterministic_trans{L}:
  */
 /*@ ghost int aorai_y = 0; */
 /*@
-lemma aorai_intermediate_state_1_deterministic_trans{L}:
+check lemma aorai_intermediate_state_1_deterministic_trans{L}:
   ¬(\at(aorai_CurOperation,L) ≡ op_g ∧
      \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
      \at(aorai_y,L) ≡ 2 ∧
@@ -68,7 +68,7 @@ lemma aorai_intermediate_state_1_deterministic_trans{L}:
  */
 /*@ ghost int aorai_x = 0; */
 /*@
-lemma aorai_intermediate_state_deterministic_trans{L}:
+check lemma aorai_intermediate_state_deterministic_trans{L}:
   ¬(\at(aorai_CurOperation,L) ≡ op_f ∧
      \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
      \at(aorai_x,L) ≡ 1 ∧

src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle

@@ -15,7 +15,7 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ lemma s0_deterministic_trans{L}: \true;
+/*@ check lemma s0_deterministic_trans{L}: \true;
  */
 int f(void);
 

src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle

@@ -19,19 +19,19 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
-/*@ lemma aorai_reject_deterministic_trans{L}: \true;
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
  */
 /*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
 /*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
 /*@
-lemma aorai_intermediate_state_deterministic_trans{L}:
+check lemma aorai_intermediate_state_deterministic_trans{L}:
   ¬(\at(aorai_CurOperation,L) ≡ op_main ∧
      \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
      ¬(\at(aorai_CurOperation,L) ≡ op_main ∧
         \at(aorai_CurOpStatus,L) ≡ aorai_Terminated));
  */
 /*@
-lemma Init_deterministic_trans{L}:
+check lemma Init_deterministic_trans{L}:
   ¬(\at(aorai_CurOperation,L) ≡ op_main ∧
      \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
      ¬(\at(aorai_CurOperation,L) ≡ op_main ∧