diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index c4a7cda302fa5898223e82526a6a5c61f8154745..44ef64c7d1d270711e4959275da491627760735a 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -1822,14 +1822,17 @@ let mk_stmt loc (states, tr) f fst status ((st,_) as state) res =
         (List.rev exp_from_trans)
         (List.rev stmt_from_action)
     else
-      List.fold_left2
-        (fun acc cond stmt_act ->
-           if stmt_act = [] then acc
-           else
-             (mkIfStmt cond (mkBlock stmt_act) (mkBlock []))::acc)
-        [mkIfStmt if_cond (mkBlock [then_stmt]) (mkBlock else_stmt)]
-        (List.rev exp_from_trans)
-        (List.rev stmt_from_action)
+      let actions =
+        List.fold_left2
+          (fun acc cond stmt_act ->
+             if stmt_act = [] then acc
+             else
+               (mkIfStmt cond (mkBlock stmt_act) (mkBlock []))::acc)
+          []
+          (List.rev exp_from_trans)
+          (List.rev stmt_from_action)
+      in
+      mkIfStmt if_cond (mkBlock [then_stmt]) (mkBlock else_stmt) :: actions
   end else
   if Aorai_option.Deterministic.get () then []
   else [is_out_of_state_stmt state loc]
diff --git a/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle
index f4ec0edda45a5b3cdb0edf3b601818f2689d2653..be1dc66d50a67adc2e0084901bd3f42750112477 100644
--- a/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle
@@ -91,15 +91,15 @@ 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_0 == 1) 
-      if (aorai_counter < 5) aorai_counter ++;
-    if (aorai_intermediate_state == 1) aorai_counter = 1;
     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;
     Sf_tmp = 0;
diff --git a/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle b/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle
index 5fc4bc1ae7b69ebef9e6addbf82dc6d42867862d..a5cacc4f933d918b45b6edc55ad5f29a5fae441f 100644
--- a/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle
@@ -273,10 +273,6 @@ void f(void)
     aorai_intermediate_state_1_tmp = aorai_intermediate_state_1;
     aorai_intermediate_state_2_tmp = aorai_intermediate_state_2;
     aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
-    if (aorai_intermediate_state_2 == 1) 
-      if (aorai_counter < 2) aorai_counter ++;
-    if (aorai_intermediate_state_0 == 1) aorai_counter = 1;
-    if (aorai_intermediate_state == 1) aorai_counter = 1;
     if (aorai_intermediate_state == 1) aorai_intermediate_state_3_tmp = 1;
     else 
       if (aorai_intermediate_state_0 == 1) aorai_intermediate_state_3_tmp = 1;
@@ -285,6 +281,10 @@ void f(void)
           if (aorai_counter < 2) aorai_intermediate_state_3_tmp = 1;
           else aorai_intermediate_state_3_tmp = 0;
         else aorai_intermediate_state_3_tmp = 0;
+    if (aorai_intermediate_state_2 == 1) 
+      if (aorai_counter < 2) aorai_counter ++;
+    if (aorai_intermediate_state_0 == 1) aorai_counter = 1;
+    if (aorai_intermediate_state == 1) aorai_counter = 1;
     aorai_intermediate_state_2_tmp = 0;
     aorai_intermediate_state_1_tmp = 0;
     aorai_intermediate_state_0_tmp = 0;
diff --git a/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle
index d2de21821b3d81ed010a05d33dee104216f8102d..ee365599daca21839bef129193e1c900b8b41a3a 100644
--- a/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle
@@ -91,15 +91,15 @@ 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_0 == 1) 
-      if (aorai_counter < 5) aorai_counter ++;
-    if (aorai_intermediate_state == 1) aorai_counter = 1;
     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;
     Sf_tmp = 0;
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle b/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle
index 7800d93810c2a947f410410abee6417f5f347ceb..92104920d5c8adb5c661dc1d9b2aad3ecd67d897 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle
@@ -2,5 +2,3 @@
 [aorai] Welcome to the Aorai plugin
 [kernel] Parsing /tmp/aorai_loop_bts1050_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
-  1 ≡ aorai_intermediate_state_1 in automaton function f_pre_func
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle b/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle
index 7c1aab1abe4f54ad288f51e3bd26f924bf512108..ab5514b69d283470a1e2184cdcc12e63f8ebb982 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle
@@ -2,5 +2,3 @@
 [aorai] Welcome to the Aorai plugin
 [kernel] Parsing /tmp/aorai_seq_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
-  1 ≡ aorai_intermediate_state_3 in automaton function g_pre_func
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle b/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle
index 91bbf9123ac28316d201cdf502362adf55674962..64b2e8b35400831ed2002e84f81fae3ae841e55f 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle
@@ -2,5 +2,3 @@
 [aorai] Welcome to the Aorai plugin
 [kernel] Parsing /tmp/aorai_seq_loop_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
-  1 ≡ aorai_intermediate_state_1 in automaton function f_pre_func