[aorai] update oracles

src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle

@@ -52,8 +52,9 @@ extern int call_to_an_undefined_function(void);
     T0_S2_tmp = T0_S2;
     T0_init_tmp = T0_init;
     accept_S1_tmp = accept_S1;
-    if (T0_S2 == 1 || accept_S1 == 1) accept_S1_tmp = 1;
-    else accept_S1_tmp = 0;
+    if (T0_S2 == 1) accept_S1_tmp = 1;
+    else 
+      if (accept_S1 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
     T0_init_tmp = 0;
     T0_S2_tmp = 0;
     T0_S2 = T0_S2_tmp;
@@ -160,7 +161,9 @@ int a(void)
     accept_S1_tmp = accept_S1;
     accept_S1_tmp = 0;
     T0_init_tmp = 0;
-    if (T0_S2 == 1 || accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+    if (T0_S2 == 1) T0_S2_tmp = 1;
+    else 
+      if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
     T0_S2 = T0_S2_tmp;
     T0_init = T0_init_tmp;
     accept_S1 = accept_S1_tmp;

src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle

@@ -274,10 +274,12 @@ int commit_trans(void)
     accept_S4_tmp = accept_S4;
     accept_init_tmp = accept_init;
     accept_init_tmp = 0;
-    if (accept_S2 == 1 && status != 0) accept_S4_tmp = 1;
+    if (accept_S2 == 1) 
+      if (status != 0) accept_S4_tmp = 1; else accept_S4_tmp = 0;
     else accept_S4_tmp = 0;
     accept_S3_tmp = 0;
-    if (accept_S2 == 1 && status == 0) accept_S2_tmp = 1;
+    if (accept_S2 == 1) 
+      if (status == 0) accept_S2_tmp = 1; else accept_S2_tmp = 0;
     else accept_S2_tmp = 0;
     accept_S1_tmp = 0;
     accept_S1 = accept_S1_tmp;

src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle

@@ -145,7 +145,9 @@ int rr = 1;
     accept_all_tmp = 0;
     accept_S5_tmp = 0;
     accept_S4_tmp = 0;
-    if (T0_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
+    if (T0_S2 == 1) 
+      if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
+    else accept_S3_tmp = 0;
     T0_init_tmp = 0;
     if (T0_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
     T0_S2 = T0_S2_tmp;

src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle

@@ -238,7 +238,9 @@ void opa(void)
     accept_S3_tmp = accept_S3;
     accept_all_tmp = accept_all;
     accept_all_tmp = 0;
-    if (T1_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
+    if (T1_S2 == 1) 
+      if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
+    else accept_S3_tmp = 0;
     T1_S2_tmp = 0;
     T0_init_tmp = 0;
     T0_S4_tmp = 0;

src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle

@@ -219,8 +219,9 @@ int decode_int(char *s)
     accept_S2_tmp = accept_S2;
     accept_init_tmp = accept_init;
     accept_init_tmp = 0;
-    if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
-    else accept_S2_tmp = 0;
+    if (accept_S1 == 1) accept_S2_tmp = 1;
+    else 
+      if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
     accept_S1_tmp = 0;
     accept_S1 = accept_S1_tmp;
     accept_S2 = accept_S2_tmp;
@@ -268,10 +269,12 @@ int decode_int(char *s)
     accept_S2_tmp = accept_S2;
     accept_init_tmp = accept_init;
     accept_init_tmp = 0;
-    if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
-    else accept_S2_tmp = 0;
-    if (accept_S1 == 1 || accept_S2 == 1) accept_S1_tmp = 1;
-    else accept_S1_tmp = 0;
+    if (accept_S1 == 1) accept_S2_tmp = 1;
+    else 
+      if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+    if (accept_S1 == 1) accept_S1_tmp = 1;
+    else 
+      if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
     accept_S1 = accept_S1_tmp;
     accept_S2 = accept_S2_tmp;
     accept_init = accept_init_tmp;

src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle

@@ -106,7 +106,11 @@ int global_argc = 0;
     accept_T2_tmp = 0;
     T1_tmp = 0;
     T0_init_tmp = 0;
-    if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
+    if (S1 == 1) S1_tmp = 1;
+    else 
+      if (T1 == 1) 
+        if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
+      else S1_tmp = 0;
     S1 = S1_tmp;
     T0_init = T0_init_tmp;
     T1 = T1_tmp;

src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle

@@ -106,7 +106,11 @@ int global_argc = 0;
     accept_T2_tmp = 0;
     T1_tmp = 0;
     T0_init_tmp = 0;
-    if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
+    if (S1 == 1) S1_tmp = 1;
+    else 
+      if (T1 == 1) 
+        if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
+      else S1_tmp = 0;
     S1 = S1_tmp;
     T0_init = T0_init_tmp;
     T1 = T1_tmp;
@@ -420,7 +424,9 @@ int sumOne(char *t, int length)
     T0_init_tmp = T0_init;
     T1_tmp = T1;
     accept_T2_tmp = accept_T2;
-    if (T1 == 1 && res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0;
+    if (T1 == 1) 
+      if (res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0;
+    else accept_T2_tmp = 0;
     if (T1 == 1) T1_tmp = 1; else T1_tmp = 0;
     T0_init_tmp = 0;
     S1_tmp = 0;

src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle

@@ -58,7 +58,9 @@ enum aorai_OpStatusList {
     accept_S2_tmp = 0;
     accept_S1_tmp = 0;
     T0_init_tmp = 0;
-    if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+    if (T0_S2 == 1) T0_S2_tmp = 1;
+    else 
+      if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
     T0_S2 = T0_S2_tmp;
     T0_init = T0_init_tmp;
     accept_S1 = accept_S1_tmp;
@@ -250,10 +252,14 @@ int countOne(char *argv)
     T0_init_tmp = T0_init;
     accept_S1_tmp = accept_S1;
     accept_S2_tmp = accept_S2;
-    if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
-    else accept_S2_tmp = 0;
-    if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
-    else accept_S1_tmp = 0;
+    if (T0_S2 == 1) accept_S2_tmp = 1;
+    else 
+      if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+    if (T0_S2 == 1) accept_S1_tmp = 1;
+    else 
+      if (accept_S1 == 1) accept_S1_tmp = 1;
+      else 
+        if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
     T0_init_tmp = 0;
     if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
     T0_S2 = T0_S2_tmp;

src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle

@@ -58,7 +58,9 @@ enum aorai_OpStatusList {
     accept_S2_tmp = 0;
     accept_S1_tmp = 0;
     T0_init_tmp = 0;
-    if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+    if (T0_S2 == 1) T0_S2_tmp = 1;
+    else 
+      if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
     T0_S2 = T0_S2_tmp;
     T0_init = T0_init_tmp;
     accept_S1 = accept_S1_tmp;
@@ -248,10 +250,14 @@ int countOne(char *argv)
     T0_init_tmp = T0_init;
     accept_S1_tmp = accept_S1;
     accept_S2_tmp = accept_S2;
-    if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
-    else accept_S2_tmp = 0;
-    if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
-    else accept_S1_tmp = 0;
+    if (T0_S2 == 1) accept_S2_tmp = 1;
+    else 
+      if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+    if (T0_S2 == 1) accept_S1_tmp = 1;
+    else 
+      if (accept_S1 == 1) accept_S1_tmp = 1;
+      else 
+        if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
     T0_init_tmp = 0;
     if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
     T0_S2 = T0_S2_tmp;

src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle

@@ -58,7 +58,9 @@ enum aorai_OpStatusList {
     accept_S2_tmp = 0;
     accept_S1_tmp = 0;
     T0_init_tmp = 0;
-    if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+    if (T0_S2 == 1) T0_S2_tmp = 1;
+    else 
+      if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
     T0_S2 = T0_S2_tmp;
     T0_init = T0_init_tmp;
     accept_S1 = accept_S1_tmp;
@@ -255,10 +257,14 @@ int countOne(char *argv)
     T0_init_tmp = T0_init;
     accept_S1_tmp = accept_S1;
     accept_S2_tmp = accept_S2;
-    if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
-    else accept_S2_tmp = 0;
-    if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
-    else accept_S1_tmp = 0;
+    if (T0_S2 == 1) accept_S2_tmp = 1;
+    else 
+      if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+    if (T0_S2 == 1) accept_S1_tmp = 1;
+    else 
+      if (accept_S1 == 1) accept_S1_tmp = 1;
+      else 
+        if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
     T0_init_tmp = 0;
     if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
     T0_S2 = T0_S2_tmp;

src/plugins/aorai/tests/ya/logical_operators.i

 /* 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@
 */
 
 void f(int x) {}

src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle

@@ -42,8 +42,15 @@ enum aorai_OpStatusList {
     aorai_CurOperation = op_main;
     S0_tmp = S0;
     S1_tmp = S1;
-    if (S0 == 1 && s->x >= 0 || S0 == 1 && s->x < 0) S1_tmp = 1;
-    else S1_tmp = 0;
+    if (S0 == 1) {
+      if (s->x >= 0) S1_tmp = 1; else goto __aorai_label;
+    }
+    else {
+      __aorai_label: ;
+      if (S0 == 1) 
+        if (s->x < 0) S1_tmp = 1; else S1_tmp = 0;
+      else S1_tmp = 0;
+    }
     S0_tmp = 0;
     S0 = S0_tmp;
     S1 = S1_tmp;

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

@@ -112,10 +112,16 @@ check lemma S0_deterministic_trans{L}:
     /@ slevel full; @/
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_g;
-    if (3 == aorai_CurStates && x == 4) aorai_CurStates = S4;
-    else 
-      if (3 == aorai_CurStates && x == 5) aorai_CurStates = S5;
+    if (3 == aorai_CurStates) {
+      if (x == 4) aorai_CurStates = S4; else goto __aorai_label;
+    }
+    else {
+      __aorai_label: ;
+      if (3 == aorai_CurStates) 
+        if (x == 5) aorai_CurStates = S5;
+        else aorai_CurStates = aorai_reject;
       else aorai_CurStates = aorai_reject;
+    }
     return;
   }
 
@@ -241,7 +247,8 @@ void g(int x)
     /@ slevel full; @/
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
-    if (1 == aorai_CurStates && x == 4) aorai_CurStates = S3;
+    if (1 == aorai_CurStates) 
+      if (x == 4) aorai_CurStates = S3; else aorai_CurStates = aorai_reject;
     else aorai_CurStates = aorai_reject;
     return;
   }
@@ -292,7 +299,11 @@ void g(int x)
     /@ slevel full; @/
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
-    if (1 == aorai_CurStates && (res == 0 && X == 5)) aorai_CurStates = S2;
+    if (1 == aorai_CurStates) 
+      if (res == 0) 
+        if (X == 5) aorai_CurStates = S2;
+        else aorai_CurStates = aorai_reject;
+      else aorai_CurStates = aorai_reject;
     else aorai_CurStates = aorai_reject;
     return;
   }
@@ -368,10 +379,16 @@ int f(int x)
     /@ slevel full; @/
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_real_main;
-    if (0 == aorai_CurStates && c != 0) aorai_CurStates = S1;
-    else 
-      if (0 == aorai_CurStates && c == 0) aorai_CurStates = S2;
+    if (0 == aorai_CurStates) {
+      if (c != 0) aorai_CurStates = S1; else goto __aorai_label_0;
+    }
+    else {
+      __aorai_label_0: ;
+      if (0 == aorai_CurStates) 
+        if (c == 0) aorai_CurStates = S2;
+        else aorai_CurStates = aorai_reject;
       else aorai_CurStates = aorai_reject;
+    }
     return;
   }
 

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

@@ -131,16 +131,23 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
     /@ slevel full; @/
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
-    if (7 == aorai_CurStates && x == 1) {
-      aorai_CurStates = aorai_intermediate_state;
-      aorai_x = x;
-    }
-    else 
-      if (7 == aorai_CurStates && x == 3) {
-        aorai_CurStates = aorai_intermediate_state_2;
-        aorai_x_0 = x;
+    if (7 == aorai_CurStates) {
+      if (x == 1) {
+        aorai_CurStates = aorai_intermediate_state;
+        aorai_x = x;
       }
+      else goto __aorai_label;
+    }
+    else {
+      __aorai_label: ;
+      if (7 == aorai_CurStates) 
+        if (x == 3) {
+          aorai_CurStates = aorai_intermediate_state_2;
+          aorai_x_0 = x;
+        }
+        else aorai_CurStates = aorai_reject;
       else aorai_CurStates = aorai_reject;
+    }
     return;
   }
 
@@ -214,14 +221,30 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
     /@ slevel full; @/
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
-    if (4 == aorai_CurStates && aorai_x_0 == 3) aorai_CurStates = OK;
-    else 
-      if (1 == aorai_CurStates && aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
-      else 
-        if (4 == aorai_CurStates && aorai_x_0 != 3) aorai_CurStates = aorai_reject;
-        else 
-          if (1 == aorai_CurStates && aorai_x != 1) aorai_CurStates = aorai_reject;
+    if (4 == aorai_CurStates) {
+      if (aorai_x_0 == 3) aorai_CurStates = OK; else goto __aorai_label_2;
+    }
+    else {
+      __aorai_label_2: ;
+      if (1 == aorai_CurStates) {
+        if (aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
+        else goto __aorai_label_1;
+      }
+      else {
+        __aorai_label_1: ;
+        if (4 == aorai_CurStates) {
+          if (aorai_x_0 != 3) aorai_CurStates = aorai_reject;
+          else goto __aorai_label_0;
+        }
+        else {
+          __aorai_label_0: ;
+          if (1 == aorai_CurStates) 
+            if (aorai_x != 1) aorai_CurStates = aorai_reject;
+            else aorai_CurStates = aorai_reject;
           else aorai_CurStates = aorai_reject;
+        }
+      }
+    }
     return;
   }
 
@@ -422,14 +445,20 @@ int f(int x)
     /@ slevel full; @/
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_g;
-    if (3 == aorai_CurStates && aorai_y == 2) aorai_CurStates = OK;
-    else 
+    if (3 == aorai_CurStates) {
+      if (aorai_y == 2) aorai_CurStates = OK; else goto __aorai_label_3;
+    }
+    else {
+      __aorai_label_3: ;
       if (0 == aorai_CurStates) aorai_CurStates = OK;
       else 
         if (5 == aorai_CurStates) aorai_CurStates = aorai_reject;
         else 
-          if (3 == aorai_CurStates && aorai_y != 2) aorai_CurStates = aorai_reject;
+          if (3 == aorai_CurStates) 
+            if (aorai_y != 2) aorai_CurStates = aorai_reject;
+            else aorai_CurStates = aorai_reject;
           else aorai_CurStates = aorai_reject;
+    }
     return;
   }
 

src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle

@@ -317,10 +317,14 @@ int main_bhv_bhv(int c); */
     aorai_reject_tmp = 0;
     aorai_intermediate_state_2_tmp = 0;
     aorai_intermediate_state_1_tmp = 0;
-    if (S0 == 1 && c <= 0) aorai_intermediate_state_0_tmp = 1;
+    if (S0 == 1) 
+      if (c <= 0) aorai_intermediate_state_0_tmp = 1;
+      else aorai_intermediate_state_0_tmp = 0;
     else aorai_intermediate_state_0_tmp = 0;
     bhv_aux = main_bhv_bhv(c);
-    if (S0 == 1 && bhv_aux) aorai_intermediate_state_tmp = 1;
+    if (S0 == 1) 
+      if (bhv_aux) aorai_intermediate_state_tmp = 1;
+      else aorai_intermediate_state_tmp = 0;
     else aorai_intermediate_state_tmp = 0;
     Sf_tmp = 0;
     S0_tmp = 0;
@@ -409,17 +413,25 @@ int main_bhv_bhv(int c); */
     aorai_intermediate_state_1_tmp = aorai_intermediate_state_1;
     aorai_intermediate_state_2_tmp = aorai_intermediate_state_2;
     aorai_reject_tmp = aorai_reject;
-    if ((aorai_intermediate_state_0 == 1 || aorai_intermediate_state_2 == 1 && 
-                                            res != 0) || aorai_reject == 1) 
-      aorai_reject_tmp = 1;
-    else aorai_reject_tmp = 0;
+    if (aorai_intermediate_state_0 == 1) aorai_reject_tmp = 1;
+    else 
+      if (aorai_intermediate_state_2 == 1) {
+        if (res != 0) aorai_reject_tmp = 1; else goto __aorai_label;
+      }
+      else {
+        __aorai_label: ;
+        if (aorai_reject == 1) aorai_reject_tmp = 1;
+        else aorai_reject_tmp = 0;
+      }
     aorai_intermediate_state_2_tmp = 0;
     aorai_intermediate_state_1_tmp = 0;
     aorai_intermediate_state_0_tmp = 0;
     aorai_intermediate_state_tmp = 0;
-    if (aorai_intermediate_state == 1 || aorai_intermediate_state_2 == 1 && 
-                                         res == 0) Sf_tmp = 1;
-    else Sf_tmp = 0;
+    if (aorai_intermediate_state == 1) Sf_tmp = 1;
+    else 
+      if (aorai_intermediate_state_2 == 1) 
+        if (res == 0) Sf_tmp = 1; else Sf_tmp = 0;
+      else Sf_tmp = 0;
     S0_tmp = 0;
     S0 = S0_tmp;
     Sf = Sf_tmp;

src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle

 [kernel] Parsing tests/ya/logical_operators.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_logical_operators_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
@@ -10,8 +9,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 I = 1; */
 /*@ ghost
   /@ requires 1 ≡ I;
@@ -31,6 +30,7 @@ enum aorai_OpStatusList {
   void f_pre_func(int x)
   {
     int I_tmp;
+    /@ slevel full; @/
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_f;
     I_tmp = I;
@@ -66,6 +66,7 @@ enum aorai_OpStatusList {
   void f_post_func(void)
   {
     int I_tmp;
+    /@ slevel full; @/
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_f;
     I_tmp = I;
@@ -107,6 +108,7 @@ void f(int x)
   void main_pre_func(int x)
   {
     int I_tmp;
+    /@ slevel full; @/
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_main;
     I_tmp = I;
@@ -134,6 +136,7 @@ void f(int x)
   void main_post_func(void)
   {
     int I_tmp;
+    /@ slevel full; @/
     aorai_CurOpStatus = aorai_Terminated;
     aorai_CurOperation = op_main;
     I_tmp = I;

src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle

@@ -95,10 +95,14 @@ enum aorai_OpStatusList {
     aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
     aorai_intermediate_state_3_tmp = 0;
     aorai_intermediate_state_2_tmp = 0;
-    if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1 && 
-                                         aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
-    else aorai_intermediate_state_1_tmp = 0;
-    if (aorai_intermediate_state_0 == 1 && aorai_counter < 5) aorai_counter ++;
+    if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1;
+    else 
+      if (aorai_intermediate_state_0 == 1) 
+        if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
+        else aorai_intermediate_state_1_tmp = 0;
+      else aorai_intermediate_state_1_tmp = 0;
+    if (aorai_intermediate_state_0 == 1) 
+      if (aorai_counter < 5) aorai_counter ++;
     if (aorai_intermediate_state == 1) aorai_counter = 1;
     aorai_intermediate_state_0_tmp = 0;
     aorai_intermediate_state_tmp = 0;
@@ -544,9 +548,9 @@ void g(void)
     aorai_intermediate_state_1_tmp = 0;
     aorai_intermediate_state_0_tmp = 0;
     aorai_intermediate_state_tmp = 0;
-    if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1) 
-      Sf_tmp = 1;
-    else Sf_tmp = 0;
+    if (aorai_intermediate_state == 1) Sf_tmp = 1;
+    else 
+      if (aorai_intermediate_state_0 == 1) Sf_tmp = 1; else Sf_tmp = 0;
     S0_tmp = 0;
     S0 = S0_tmp;
     Sf = Sf_tmp;

src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle

@@ -363,7 +363,9 @@ void g(void)
     /@ slevel full; @/
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_h;
-    if (5 == aorai_CurStates && aorai_x > 0) aorai_CurStates = f_0;
+    if (5 == aorai_CurStates) 
+      if (aorai_x > 0) aorai_CurStates = f_0;
+      else aorai_CurStates = aorai_reject;
     else aorai_CurStates = aorai_reject;
     return;
   }

src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle

@@ -39,7 +39,9 @@ enum aorai_OpStatusList {
     aorai_CurOperation = op_f;
     S0_tmp = S0;
     Sf_tmp = Sf;
-    if (S0 == 1 && x >= 4) Sf_tmp = 1; else Sf_tmp = 0;
+    if (S0 == 1) 
+      if (x >= 4) Sf_tmp = 1; else Sf_tmp = 0;
+    else Sf_tmp = 0;
     S0_tmp = 0;
     S0 = S0_tmp;
     Sf = Sf_tmp;

src/plugins/aorai/tests/ya/oracle/other.res.oracle

@@ -65,13 +65,42 @@ int x = 0;
     init_tmp = init;
     last_tmp = last;
     step1_tmp = step1;
-    if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4) 
-      step1_tmp = 1;
-    else step1_tmp = 0;
-    if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
-    else last_tmp = 0;
-    if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
-    else init_tmp = 0;
+    if (init == 1) {
+      if (x == 3) step1_tmp = 1; else goto __aorai_label_2;
+    }
+    else {
+      __aorai_label_2: ;
+      if (last == 1) {
+        if (x == 3) step1_tmp = 1; else goto __aorai_label_1;
+      }
+      else {
+        __aorai_label_1: ;
+        if (step1 == 1) 
+          if (x != 4) step1_tmp = 1; else step1_tmp = 0;
+        else step1_tmp = 0;
+      }
+    }
+    if (last == 1) {
+      if (x != 4) {
+        if (x != 3) last_tmp = 1; else goto __aorai_label_0;
+      }
+      else goto __aorai_label_0;
+    }
+    else {
+      __aorai_label_0: ;
+      if (step1 == 1) 
+        if (x == 4) last_tmp = 1; else last_tmp = 0;
+      else last_tmp = 0;
+    }
+    if (init == 1) {
+      if (x != 3) init_tmp = 1; else goto __aorai_label;
+    }
+    else {
+      __aorai_label: ;
+      if (last == 1) 
+        if (x == 4) init_tmp = 1; else init_tmp = 0;
+      else init_tmp = 0;
+    }
     init = init_tmp;
     last = last_tmp;
     step1 = step1_tmp;
@@ -129,13 +158,42 @@ int x = 0;
     init_tmp = init;
     last_tmp = last;
     step1_tmp = step1;
-    if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4) 
-      step1_tmp = 1;
-    else step1_tmp = 0;
-    if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
-    else last_tmp = 0;
-    if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
-    else init_tmp = 0;
+    if (init == 1) {
+      if (x == 3) step1_tmp = 1; else goto __aorai_label_6;
+    }
+    else {
+      __aorai_label_6: ;
+      if (last == 1) {
+        if (x == 3) step1_tmp = 1; else goto __aorai_label_5;
+      }
+      else {
+        __aorai_label_5: ;
+        if (step1 == 1) 
+          if (x != 4) step1_tmp = 1; else step1_tmp = 0;
+        else step1_tmp = 0;
+      }
+    }
+    if (last == 1) {
+      if (x != 4) {
+        if (x != 3) last_tmp = 1; else goto __aorai_label_4;
+      }
+      else goto __aorai_label_4;
+    }
+    else {
+      __aorai_label_4: ;
+      if (step1 == 1) 
+        if (x == 4) last_tmp = 1; else last_tmp = 0;
+      else last_tmp = 0;
+    }
+    if (init == 1) {
+      if (x != 3) init_tmp = 1; else goto __aorai_label_3;
+    }
+    else {
+      __aorai_label_3: ;
+      if (last == 1) 
+        if (x == 4) init_tmp = 1; else init_tmp = 0;
+      else init_tmp = 0;
+    }
     init = init_tmp;
     last = last_tmp;
     step1 = step1_tmp;
@@ -257,13 +315,42 @@ void f(void)
     init_tmp = init;
     last_tmp = last;
     step1_tmp = step1;
-    if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4) 
-      step1_tmp = 1;
-    else step1_tmp = 0;
-    if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
-    else last_tmp = 0;
-    if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
-    else init_tmp = 0;
+    if (init == 1) {
+      if (x == 3) step1_tmp = 1; else goto __aorai_label_10;
+    }
+    else {
+      __aorai_label_10: ;
+      if (last == 1) {
+        if (x == 3) step1_tmp = 1; else goto __aorai_label_9;
+      }
+      else {
+        __aorai_label_9: ;
+        if (step1 == 1) 
+          if (x != 4) step1_tmp = 1; else step1_tmp = 0;
+        else step1_tmp = 0;
+      }
+    }
+    if (last == 1) {
+      if (x != 4) {
+        if (x != 3) last_tmp = 1; else goto __aorai_label_8;
+      }
+      else goto __aorai_label_8;
+    }
+    else {
+      __aorai_label_8: ;
+      if (step1 == 1) 
+        if (x == 4) last_tmp = 1; else last_tmp = 0;
+      else last_tmp = 0;
+    }
+    if (init == 1) {
+      if (x != 3) init_tmp = 1; else goto __aorai_label_7;
+    }
+    else {
+      __aorai_label_7: ;
+      if (last == 1) 
+        if (x == 4) init_tmp = 1; else init_tmp = 0;
+      else init_tmp = 0;
+    }
     init = init_tmp;
     last = last_tmp;
     step1 = step1_tmp;
@@ -321,13 +408,42 @@ void f(void)
     init_tmp = init;
     last_tmp = last;
     step1_tmp = step1;
-    if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4) 
-      step1_tmp = 1;
-    else step1_tmp = 0;
-    if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
-    else last_tmp = 0;
-    if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
-    else init_tmp = 0;
+    if (init == 1) {
+      if (x == 3) step1_tmp = 1; else goto __aorai_label_14;
+    }
+    else {
+      __aorai_label_14: ;
+      if (last == 1) {
+        if (x == 3) step1_tmp = 1; else goto __aorai_label_13;
+      }
+      else {
+        __aorai_label_13: ;
+        if (step1 == 1) 
+          if (x != 4) step1_tmp = 1; else step1_tmp = 0;
+        else step1_tmp = 0;
+      }
+    }
+    if (last == 1) {
+      if (x != 4) {
+        if (x != 3) last_tmp = 1; else goto __aorai_label_12;
+      }
+      else goto __aorai_label_12;
+    }
+    else {
+      __aorai_label_12: ;
+      if (step1 == 1) 
+        if (x == 4) last_tmp = 1; else last_tmp = 0;
+      else last_tmp = 0;
+    }
+    if (init == 1) {
+      if (x != 3) init_tmp = 1; else goto __aorai_label_11;
+    }
+    else {
+      __aorai_label_11: ;
+      if (last == 1) 
+        if (x == 4) init_tmp = 1; else init_tmp = 0;
+      else init_tmp = 0;
+    }
     init = init_tmp;
     last = last_tmp;
     step1 = step1_tmp;
@@ -436,9 +552,13 @@ void g(void)
     init_tmp = init;
     last_tmp = last;
     step1_tmp = step1;
-    if (init == 1 && x == 3) step1_tmp = 1; else step1_tmp = 0;
+    if (init == 1) 
+      if (x == 3) step1_tmp = 1; else step1_tmp = 0;
+    else step1_tmp = 0;
     last_tmp = 0;
-    if (init == 1 && x != 3) init_tmp = 1; else init_tmp = 0;
+    if (init == 1) 
+      if (x != 3) init_tmp = 1; else init_tmp = 0;
+    else init_tmp = 0;
     init = init_tmp;
     last = last_tmp;
     step1 = step1_tmp;
@@ -496,13 +616,42 @@ void g(void)
     init_tmp = init;
     last_tmp = last;
     step1_tmp = step1;
-    if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4) 
-      step1_tmp = 1;
-    else step1_tmp = 0;
-    if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
-    else last_tmp = 0;
-    if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
-    else init_tmp = 0;
+    if (init == 1) {
+      if (x == 3) step1_tmp = 1; else goto __aorai_label_18;
+    }
+    else {
+      __aorai_label_18: ;
+      if (last == 1) {
+        if (x == 3) step1_tmp = 1; else goto __aorai_label_17;
+      }
+      else {
+        __aorai_label_17: ;
+        if (step1 == 1) 
+          if (x != 4) step1_tmp = 1; else step1_tmp = 0;
+        else step1_tmp = 0;
+      }
+    }
+    if (last == 1) {
+      if (x != 4) {
+        if (x != 3) last_tmp = 1; else goto __aorai_label_16;
+      }
+      else goto __aorai_label_16;
+    }
+    else {
+      __aorai_label_16: ;
+      if (step1 == 1) 
+        if (x == 4) last_tmp = 1; else last_tmp = 0;
+      else last_tmp = 0;
+    }
+    if (init == 1) {
+      if (x != 3) init_tmp = 1; else goto __aorai_label_15;
+    }
+    else {
+      __aorai_label_15: ;
+      if (last == 1) 
+        if (x == 4) init_tmp = 1; else init_tmp = 0;
+      else init_tmp = 0;
+    }
     init = init_tmp;
     last = last_tmp;
     step1 = step1_tmp;