diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index aadd8a359bd7eada4f5cd551479310ebe84c2024..08dff72aecdaf42f1a9270efab1c75ed5bcc4fa1 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -560,21 +560,6 @@ class visit_adding_pre_post_from_buch treatloops =
       predicate_to_invariant kf stmt pred
     end
   in
-  let impossible_states_preds start possible_states my_state =
-    let treat_one_start_state state start_state end_states acc =
-      if not (Data_for_aorai.Aorai_state.Map.mem state end_states) then
-        Logic_const.pimplies
-          (Logic_const.pat(Aorai_utils.is_state_pred start_state, start),
-           Aorai_utils.is_out_of_state_pred state)
-        :: acc
-      else acc
-    in
-    let treat_one_state state _ acc =
-      Data_for_aorai.Aorai_state.Map.fold
-        (treat_one_start_state state) my_state acc
-    in
-    Data_for_aorai.Aorai_state.Map.fold treat_one_state possible_states []
-  in
   let impossible_states_preds_inv start possible_states my_state =
     let treat_one_start_state state start_state end_states acc =
       if Data_for_aorai.Aorai_state.Map.mem state end_states then
@@ -1064,7 +1049,8 @@ class visit_adding_pre_post_from_buch treatloops =
         condition_to_invariant kf possible_states new_loop;
 
         let init_preds =
-          impossible_states_preds Logic_const.pre_label possible_states init_state
+          impossible_states_preds_inv
+            Logic_const.pre_label possible_states init_state
         in
         let treat_init_pred pred =
           let pred = mk_imply Rneq pred in
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
index 835b432fec290a8ac7d6af9bf06df049d8a77683..ad209874b35614fa854193d25ffad9a6a46f4559 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
@@ -325,8 +325,7 @@ void main(void)
       loop invariant Aorai: 0 ≡ aorai_intermediate_state_0;
       loop invariant Aorai: 0 ≡ init;
       loop invariant Aorai: 1 ≡ S ∨ 1 ≡ T;
-      loop invariant
-        Aorai: aorai_Loop_Init_4 ≢ 0 ⇒ \at(1 ≡ init,Pre) ⇒ 0 ≡ T;
+      loop invariant Aorai: aorai_Loop_Init_4 ≢ 0 ⇒ 0 ≡ T;
       loop assigns i, aorai_Loop_Init_4, aorai_CurOpStatus,
                    aorai_CurOperation, S, T, aorai_intermediate_state,
                    aorai_intermediate_state_0, init;
diff --git a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
index 87d2fbbdcfdd992dccfecec4bacf6ac7f2f57162..82b0886cf1f944358fe4e5464610230e0a09ba24 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -610,9 +610,7 @@ int main(int c)
         Aorai:
           1 ≡ aorai_intermediate_state ∨ 1 ≡ aorai_intermediate_state_0;
       loop invariant
-        Aorai:
-          aorai_Loop_Init_13 ≢ 0 ⇒
-          \at(1 ≡ S0,Pre) ⇒ 0 ≡ aorai_intermediate_state_0;
+        Aorai: aorai_Loop_Init_13 ≢ 0 ⇒ 0 ≡ aorai_intermediate_state_0;
       loop invariant
         Aorai: aorai_Loop_Init_13 ≡ 0 ⇒ 0 ≡ aorai_intermediate_state;
       loop invariant
diff --git a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
index d02c3691359cb8475a4506d89e52c66decd789fa..ffb2b1dba40beac39e7d8ae3ef6327438b971a0b 100644
--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -200,11 +200,12 @@ void g(void)
       loop invariant
         Aorai:
           aorai_Loop_Init_4 ≢ 0 ⇒
-          \at(1 ≡ aorai_intermediate_state_0,Pre) ⇒ 0 ≡ first_step;
+          \at(0 ≡ first_step,Pre) ⇒ 0 ≡ first_step;
       loop invariant
         Aorai:
           aorai_Loop_Init_4 ≢ 0 ⇒
-          \at(1 ≡ first_step,Pre) ⇒ 0 ≡ aorai_intermediate_state_0;
+          \at(0 ≡ aorai_intermediate_state_0,Pre) ⇒
+          0 ≡ aorai_intermediate_state_0;
       loop invariant
         Aorai:
           aorai_Loop_Init_4 ≡ 0 ⇒
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
index fa3c9b2b57cb927104089ebd209c2837d1093e1e..1a827b61513c68a49b04361c0baabaf72bb19e67 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -615,9 +615,7 @@ int main(int c)
         Aorai:
           1 ≡ aorai_intermediate_state ∨ 1 ≡ aorai_intermediate_state_0;
       loop invariant
-        Aorai:
-          aorai_Loop_Init_14 ≢ 0 ⇒
-          \at(1 ≡ S0,Pre) ⇒ 0 ≡ aorai_intermediate_state_0;
+        Aorai: aorai_Loop_Init_14 ≢ 0 ⇒ 0 ≡ aorai_intermediate_state_0;
       loop invariant
         Aorai: aorai_Loop_Init_14 ≡ 0 ⇒ 0 ≡ aorai_intermediate_state;
       loop invariant