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 2a20447f8799a6fc219362ee8b8cd42e862de858..e8f31d7d12c410b9fe704537bb36d02eeb706b05 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
@@ -21,6 +21,12 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, S1, s->x, s;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, S1, s->x, s;
+     assigns S0 \from aorai_CurOpStatus, aorai_CurOperation, S0, S1, s->x, s;
+     assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S0, S1, s->x, s;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -64,6 +70,12 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+     assigns S0 \from aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+     assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S0, S1;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
index e65c2a8ed2ed4483afad57769a608f614a2b1fc1..6f35fd44384ee6713e2fcba2b8c8141febfdc79c 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
@@ -24,6 +24,27 @@ int X;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
              in_main;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S_in_f
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns in_main
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -82,6 +103,27 @@ int X;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
              in_main;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S_in_f
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns in_main
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -155,6 +197,27 @@ void f(void)
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
              in_main;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S_in_f
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns in_main
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -213,6 +276,27 @@ void f(void)
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
              in_main;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns S_in_f
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
+     assigns in_main
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+             in_main;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
index e01339d6178537b48a651161ef9701c008802541..27d4f62301443e0894f519fc111dbdbd7132e1e9 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
@@ -38,6 +38,12 @@ int X;
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_S1_out:
        ensures aorai_CurStates ≢ S1;
@@ -79,6 +85,12 @@ int X;
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_S1_out:
        ensures aorai_CurStates ≢ S1;
@@ -133,6 +145,12 @@ void f(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_S1_out:
        ensures aorai_CurStates ≢ S1;
@@ -174,6 +192,12 @@ void f(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_S1_out:
        ensures aorai_CurStates ≢ S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
index 8241b35201eef70e16cb72916b0258b927d3c966..b0cac6b01b25d96355241a543e34d95d5818b2ca 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
@@ -18,6 +18,11 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_a;
      assigns aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
      
      behavior buch_state_S_out:
        ensures 0 ≡ S;
@@ -41,6 +46,11 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_a;
      assigns aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
      
      behavior buch_state_S_out:
        ensures 0 ≡ S;
@@ -75,6 +85,11 @@ void a(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
      
      behavior buch_state_S_out:
        ensures 0 ≡ S;
@@ -98,6 +113,11 @@ void a(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
      
      behavior buch_state_S_out:
        ensures 0 ≡ S;
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 ad209874b35614fa854193d25ffad9a6a46f4559..a721d8db11216ab7be3d6b63317fa08393df9473 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
@@ -24,6 +24,27 @@ enum aorai_OpStatusList {
      ensures aorai_CurOperation ≡ op_a;
      assigns aorai_CurOpStatus, aorai_CurOperation, S, T,
              aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns S
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns T
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
      
      behavior buch_state_S_out:
        ensures 0 ≡ S;
@@ -90,6 +111,27 @@ enum aorai_OpStatusList {
      ensures aorai_CurOperation ≡ op_a;
      assigns aorai_CurOpStatus, aorai_CurOperation, S, T,
              aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns S
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns T
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
      
      behavior buch_state_S_in:
        assumes 1 ≡ aorai_intermediate_state_0;
@@ -192,6 +234,27 @@ void a(void)
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S, T,
              aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns S
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns T
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
      
      behavior buch_state_S_in:
        assumes 1 ≡ init;
@@ -251,6 +314,27 @@ void a(void)
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S, T,
              aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns S
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns T
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, S, T,
+             aorai_intermediate_state, aorai_intermediate_state_0, init;
      
      behavior buch_state_S_in:
        assumes 1 ≡ S;
diff --git a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
index f2bea78fd12e050913de8a59e500c7110eca235d..8f274a98c57bbb554137167b38888f9cb9ad3ca4 100644
--- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
@@ -51,6 +51,12 @@ check lemma I_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_I_in:
        assumes aorai_CurStates ≡ I;
@@ -80,6 +86,12 @@ check lemma I_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_I_in:
        assumes aorai_CurStates ≡ I;
diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index 84e8253a128eb3d4401ecfe556c67dcd4b9307fa..8ad803dbd2282bf19797613d2ed3d27a25325221 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -69,6 +69,12 @@ check lemma S0_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_g;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
      
      behavior buch_state_S0_out:
        ensures aorai_CurStates ≢ S0;
@@ -132,6 +138,12 @@ check lemma S0_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_g;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_S0_out:
        ensures aorai_CurStates ≢ S0;
@@ -209,6 +221,12 @@ void g(int x)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
      
      behavior buch_state_S0_out:
        ensures aorai_CurStates ≢ S0;
@@ -261,6 +279,12 @@ void g(int x)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, res, X;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, res, X;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, res, X;
      
      behavior buch_state_S0_out:
        ensures aorai_CurStates ≢ S0;
@@ -336,6 +360,12 @@ int f(int x)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_real_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, c;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, c;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, c;
      
      behavior buch_state_S0_out:
        ensures aorai_CurStates ≢ S0;
@@ -399,6 +429,12 @@ int f(int x)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_real_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_S0_out:
        ensures aorai_CurStates ≢ S0;
@@ -465,6 +501,12 @@ int real_main(int c)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_S0_in:
        assumes aorai_CurStates ≡ Si;
@@ -515,6 +557,12 @@ int real_main(int c)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_S0_out:
        ensures aorai_CurStates ≢ S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index 614d489a97d3b1a2caf54b5394b9dae08a8e0c17..c37d669f42245f94696ce437ea63e1b5637551d2 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -52,7 +52,9 @@ check lemma aorai_intermediate_state_2_deterministic_trans{L}:
      \at(aorai_x_0,L) ≡ 3 ∧
      (¬(\at(aorai_CurOperation,L) ≡ op_f ∧
          \at(aorai_CurOpStatus,L) ≡ aorai_Terminated) ∨
-      \at(aorai_x_0,L) ≢ 3));
+      (\at(aorai_CurOperation,L) ≡ op_f ∧
+       \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
+       \at(aorai_x_0,L) ≢ 3)));
  */
 /*@ ghost int aorai_y = 0; */
 /*@
@@ -62,7 +64,8 @@ check lemma aorai_intermediate_state_1_deterministic_trans{L}:
      \at(aorai_y,L) ≡ 2 ∧
      (¬(\at(aorai_CurOperation,L) ≡ op_g ∧
          \at(aorai_CurOpStatus,L) ≡ aorai_Terminated) ∨
-      \at(aorai_y,L) ≢ 2));
+      (\at(aorai_CurOperation,L) ≡ op_g ∧
+       \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧ \at(aorai_y,L) ≢ 2)));
  */
 /*@ ghost int aorai_x = 0; */
 /*@
@@ -72,7 +75,8 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
      \at(aorai_x,L) ≡ 1 ∧
      (¬(\at(aorai_CurOperation,L) ≡ op_f ∧
          \at(aorai_CurOpStatus,L) ≡ aorai_Terminated) ∨
-      \at(aorai_x,L) ≢ 1));
+      (\at(aorai_CurOperation,L) ≡ op_f ∧
+       \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧ \at(aorai_x,L) ≢ 1)));
  */
 /*@ ghost
   /@ requires aorai_CurStates ≡ main_0;
@@ -81,6 +85,12 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_x_0, aorai_x, aorai_CurOpStatus, aorai_CurOperation,
              aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, x;
      
      behavior buch_state_OK_out:
        ensures aorai_CurStates ≢ OK;
@@ -166,6 +176,15 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates,
+             aorai_x_0, aorai_x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates,
+             aorai_x_0, aorai_x;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates,
+             aorai_x_0, aorai_x;
      
      behavior buch_state_OK_in:
        assumes
@@ -321,6 +340,12 @@ int f(int x)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_g;
      assigns aorai_y, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_OK_in:
        assumes aorai_CurStates ≡ OK;
@@ -395,6 +420,12 @@ int f(int x)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_g;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_y;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_y;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_y;
      
      behavior buch_state_OK_in:
        assumes
@@ -505,6 +536,12 @@ int g(int y)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_OK_out:
        ensures aorai_CurStates ≢ OK;
@@ -552,6 +589,12 @@ int g(int y)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_OK_in:
        assumes aorai_CurStates ≡ OK;
diff --git a/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle b/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
index b6ef4dfe2f3645cea8f0f058160bd2c975d71324..16e5de830ac2b2f7e5c0161f7f79d538e4b30200 100644
--- a/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
@@ -71,6 +71,12 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_in:
        assumes aorai_CurStates ≡ s1;
@@ -133,6 +139,12 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -213,6 +225,12 @@ void f(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_g;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -275,6 +293,12 @@ void f(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_g;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -355,6 +379,12 @@ void g(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -408,6 +438,12 @@ void g(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures aorai_CurStates ≢ aorai_intermediate_state;
diff --git a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
index 1ac4f7dfe672bd5b451c955cba499b0b0bace72f..34366aa9fd40d3c26130b980494067d8a27b055a 100644
--- a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
@@ -16,6 +16,11 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
      
      behavior buch_state_S_in:
        assumes 1 ≡ S;
@@ -44,6 +49,11 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S;
+     assigns S \from aorai_CurOpStatus, aorai_CurOperation, S;
      
      behavior buch_state_S_in:
        assumes 1 ≡ S;
diff --git a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
index b89d3366d307d5b93662e3e1c4a03ff2b89f0723..0c22ea3ad2c717deed55f7fd804d2d8cf012610d 100644
--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -29,6 +29,51 @@ enum aorai_OpStatusList {
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_reject;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_reject
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -112,6 +157,51 @@ enum aorai_OpStatusList {
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_reject;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
+     assigns aorai_reject
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -262,6 +352,51 @@ int main_bhv_bhv(int c); */
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_reject;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, c;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, c;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, c;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, c;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, c;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, c;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, c;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, c;
+     assigns aorai_reject
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, c;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -352,6 +487,51 @@ int main_bhv_bhv(int c); */
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_reject;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, res;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, res;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, res;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, res;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, res;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, res;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, res;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, res;
+     assigns aorai_reject
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_reject, res;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
index 8cf4803c64527658c5930f1843076fca1a9ebf7a..e69f85f246c1dd25aac610260ab32ce16e9b29a4 100644
--- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
@@ -28,6 +28,12 @@ int f(void);
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_reject_out:
        ensures aorai_CurStates ≢ aorai_reject;
@@ -51,6 +57,12 @@ int f(void);
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_reject_out:
        ensures aorai_CurStates ≢ aorai_reject;
diff --git a/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle b/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
index ab0d4e67329e1e18ec536abbacaad37df496b018..4aa48e2ee5d7fa37f6d81627004ac5e7f4955b9d 100644
--- a/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
@@ -18,6 +18,11 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, I;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, I, x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, I, x;
+     assigns I \from aorai_CurOpStatus, aorai_CurOperation, I, x;
      
      behavior buch_state_I_in:
        assumes 1 ≡ I ∧ (x ≡ 1 ∨ x ≢ 1);
@@ -54,6 +59,11 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, I;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, I;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, I;
+     assigns I \from aorai_CurOpStatus, aorai_CurOperation, I;
      
      behavior buch_state_I_in:
        assumes 1 ≡ I;
@@ -96,6 +106,11 @@ void f(int x)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, I;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, I;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, I;
+     assigns I \from aorai_CurOpStatus, aorai_CurOperation, I;
      
      behavior buch_state_I_in:
        assumes 1 ≡ I;
@@ -124,6 +139,11 @@ void f(int x)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, I;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, I;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, I;
+     assigns I \from aorai_CurOpStatus, aorai_CurOperation, I;
      
      behavior buch_state_I_in:
        assumes 1 ≡ I;
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 82b0886cf1f944358fe4e5464610230e0a09ba24..260cb460abb1c282a351d5544b232ff3f342f913 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -34,6 +34,51 @@ enum aorai_OpStatusList {
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -132,6 +177,51 @@ enum aorai_OpStatusList {
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -243,6 +333,51 @@ void f(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -321,6 +456,51 @@ void f(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -418,6 +598,51 @@ void g(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -495,6 +720,51 @@ void g(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
index 04818b8989eb079c573c4e2246b528f065cfc881..c09d670113547f3b377d5e31c0bee83e0959f4cf 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -65,6 +65,12 @@ check lemma e_deterministic_trans{L}:
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_x, aorai_y, aorai_CurOpStatus, aorai_CurOperation,
              aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
@@ -132,6 +138,12 @@ check lemma e_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
@@ -203,6 +215,12 @@ void f(int x)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_g;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
@@ -256,6 +274,12 @@ void f(int x)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_g;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
@@ -322,6 +346,12 @@ void g(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_h;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_x;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_x;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
@@ -377,6 +407,12 @@ void g(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_h;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
@@ -443,6 +479,12 @@ void h(int x)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_i;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
@@ -497,6 +539,12 @@ void h(int x)
      ensures aorai_CurOperation ≡ op_i;
      assigns aorai_y, aorai_x, aorai_CurOpStatus, aorai_CurOperation,
              aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
@@ -582,6 +630,12 @@ void i(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
@@ -635,6 +689,12 @@ void i(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index a9b448b9b7ec3c488447c1a870cb38e485d0947e..925e912d1aedd0f75d769fd62f3649e84bad8447 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -41,6 +41,12 @@ check lemma Init_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_Init_out:
        ensures aorai_CurStates ≢ Init;
@@ -79,6 +85,12 @@ check lemma Init_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_Init_out:
        ensures aorai_CurStates ≢ Init;
@@ -129,6 +141,12 @@ void f(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_Init_out:
        ensures aorai_CurStates ≢ Init;
@@ -155,6 +173,12 @@ void f(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_Init_out:
        ensures aorai_CurStates ≢ Init;
diff --git a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
index 3dedd28abb5a05be63e89a11a18a61d136278ad9..3caffe84fad47612be18e7e4c3fec7446a18c2c2 100644
--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -18,6 +18,12 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf, x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf, x;
+     assigns S0 \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf, x;
+     assigns Sf \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf, x;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -55,6 +61,12 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
+     assigns S0 \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
+     assigns Sf \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
index 85dd02e85b7d0b72606a27d7e907636cc026cdeb..e2e3a4fe94ea87191bbb7caa3162cf0bc7f927e5 100644
--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -24,6 +24,27 @@ enum aorai_OpStatusList {
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
              aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns final
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns first_step
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
      
      behavior buch_state_aorai_intermediate_state_in:
        assumes 1 ≡ init;
@@ -85,6 +106,27 @@ enum aorai_OpStatusList {
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
              aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns final
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns first_step
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures 0 ≡ aorai_intermediate_state;
@@ -233,6 +275,27 @@ void g(void)
      ensures aorai_CurOperation ≡ op_h;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
              aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns final
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns first_step
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures 0 ≡ aorai_intermediate_state;
@@ -294,6 +357,27 @@ void g(void)
      ensures aorai_CurOperation ≡ op_h;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
              aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns final
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns first_step
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_intermediate_state,
+             aorai_intermediate_state_0, final, first_step, init;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures 0 ≡ aorai_intermediate_state;
diff --git a/src/plugins/aorai/tests/ya/oracle/other.res.oracle b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
index af246c4f01e173585dc9bad7b05fafad9897d410..f83db815ae931852f8760e80e33016d64bfa76e4 100644
--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -22,6 +22,16 @@ int x = 0;
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns last
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns step1
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
      
      behavior buch_state_init_in:
        assumes (1 ≡ last ∧ x ≡ 4) ∨ (1 ≡ init ∧ x ≢ 3);
@@ -115,6 +125,16 @@ int x = 0;
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_f;
      assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns last
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns step1
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
      
      behavior buch_state_init_in:
        assumes (1 ≡ last ∧ x ≡ 4) ∨ (1 ≡ init ∧ x ≢ 3);
@@ -272,6 +292,16 @@ void f(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_g;
      assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns last
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns step1
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
      
      behavior buch_state_init_in:
        assumes (1 ≡ last ∧ x ≡ 4) ∨ (1 ≡ init ∧ x ≢ 3);
@@ -365,6 +395,16 @@ void f(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_g;
      assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns last
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns step1
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
      
      behavior buch_state_init_in:
        assumes (1 ≡ last ∧ x ≡ 4) ∨ (1 ≡ init ∧ x ≢ 3);
@@ -521,6 +561,16 @@ void g(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns last
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns step1
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
      
      behavior buch_state_init_in:
        assumes 1 ≡ init ∧ x ≢ 3;
@@ -573,6 +623,16 @@ void g(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, init, last, step1;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns init
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns last
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
+     assigns step1
+       \from aorai_CurOpStatus, aorai_CurOperation, init, last, step1, x;
      
      behavior buch_state_init_in:
        assumes (1 ≡ last ∧ x ≡ 4) ∨ (1 ≡ init ∧ x ≢ 3);
diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
index 8e4a913ae4b32fd2f3f703976ca9ab9e7c517a7f..b2f0a865f3d5c032ce7fbb3fca1f315091ada68d 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -32,6 +32,51 @@ enum aorai_OpStatusList {
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -110,6 +155,51 @@ enum aorai_OpStatusList {
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -215,6 +305,51 @@ void f(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -322,6 +457,51 @@ void f(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -443,6 +623,51 @@ void g(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -522,6 +747,51 @@ void g(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
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 1a827b61513c68a49b04361c0baabaf72bb19e67..bae62a6316898061fab0f135c5d8568de8d0e381 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -34,6 +34,51 @@ enum aorai_OpStatusList {
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -132,6 +177,51 @@ enum aorai_OpStatusList {
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -243,6 +333,51 @@ void f(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -321,6 +456,51 @@ void f(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -418,6 +598,51 @@ void g(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -495,6 +720,51 @@ void g(void)
              aorai_intermediate_state, aorai_intermediate_state_0,
              aorai_intermediate_state_1, aorai_intermediate_state_2,
              aorai_intermediate_state_3;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_1
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_2
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
+     assigns aorai_intermediate_state_3
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state, aorai_intermediate_state_0,
+             aorai_intermediate_state_1, aorai_intermediate_state_2,
+             aorai_intermediate_state_3, aorai_counter;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
index 34b512d70052d27304c093e5971904d4d1a2a1a0..db603fa1ec63d19e7e6156d9048b95b17d41d13b 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
@@ -54,6 +54,12 @@ check lemma aorai_intermediate_state_0_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_init;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_in:
        assumes aorai_CurStates ≡ b;
@@ -101,6 +107,12 @@ check lemma aorai_intermediate_state_0_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_init;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -180,6 +192,12 @@ void init(int *a, int n)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_find;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -233,6 +251,12 @@ void init(int *a, int n)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_find;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -331,6 +355,12 @@ int find(int *a, int n, int k)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures aorai_CurStates ≢ aorai_intermediate_state;
@@ -378,6 +408,12 @@ int find(int *a, int n, int k)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_aorai_intermediate_state_out:
        ensures aorai_CurStates ≢ aorai_intermediate_state;
diff --git a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
index d9c12479a3bc4398468d901bdb4fa40304a9e160..2b50360158fb85efec7991a9ae0405c2d4cf4af8 100644
--- a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
@@ -19,6 +19,21 @@ enum aorai_OpStatusList {
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
              aorai_intermediate_state;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
@@ -63,6 +78,21 @@ enum aorai_OpStatusList {
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
              aorai_intermediate_state;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state;
+     assigns S0
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state;
+     assigns Sf
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state;
+     assigns aorai_intermediate_state
+       \from aorai_CurOpStatus, aorai_CurOperation, S0, Sf,
+             aorai_intermediate_state;
      
      behavior buch_state_S0_out:
        ensures 0 ≡ S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
index 380fab90eaab0ad21dbd51c809d46c5657beed7b..d717c70ab7b748be473e7a0955c84cfcc0b6db66 100644
--- a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
@@ -33,6 +33,12 @@ enum aorai_OpStatusList {
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_x, aorai_y, aorai_CurOpStatus, aorai_CurOperation,
              aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
@@ -83,6 +89,12 @@ enum aorai_OpStatusList {
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_x, aorai_y, aorai_CurOpStatus, aorai_CurOperation,
              aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_a_out:
        ensures aorai_CurStates ≢ a;
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index db9b5c07770a2459c6e60e83f01ceffb751a731a..cb79a5bd6d3f22ae4aa1fa8937b34a8114114863 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -59,6 +59,12 @@ check lemma emptying_stack_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_push;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_accept_out:
        ensures aorai_CurStates ≢ accept;
@@ -107,6 +113,12 @@ check lemma emptying_stack_deterministic_trans{L}:
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_push;
      assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_accept_out:
        ensures aorai_CurStates ≢ accept;
@@ -187,6 +199,12 @@ void push(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_pop;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
      
      behavior buch_state_accept_out:
        ensures aorai_CurStates ≢ accept;
@@ -235,6 +253,12 @@ void push(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_pop;
      assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, aorai_n;
      
      behavior buch_state_accept_out:
        ensures aorai_CurStates ≢ accept;
@@ -333,6 +357,12 @@ void pop(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_accept_out:
        ensures aorai_CurStates ≢ accept;
@@ -385,6 +415,12 @@ void pop(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     assigns aorai_CurStates
+       \from aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
      
      behavior buch_state_accept_in:
        assumes aorai_CurStates ≡ empty_stack;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
index 6099fd70578cc2e95d2d768aa408d629dbb114ab..c2fc72913e5f6c258e29064424942812828bf85e 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
@@ -31,6 +31,30 @@ int rr = 1;
      ensures aorai_CurOperation ≡ op_opa;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
              mainst;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, i;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, i;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, i;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, i;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, i;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, i;
+     assigns SF
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, i;
+     assigns mainst
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, i;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -99,6 +123,30 @@ int rr = 1;
      ensures aorai_CurOperation ≡ op_opa;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
              mainst;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns SF
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns mainst
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -187,6 +235,30 @@ void opa(int i, int j)
      ensures aorai_CurOperation ≡ op_opb;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
              mainst;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns SF
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns mainst
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -254,6 +326,30 @@ void opa(int i, int j)
      ensures aorai_CurOperation ≡ op_opb;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
              mainst;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, res;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, res;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, res;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, res;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, res;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, res;
+     assigns SF
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, res;
+     assigns mainst
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst, res;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -342,6 +438,30 @@ int opb(void)
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
              mainst;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns SF
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns mainst
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
      
      behavior buch_state_S1_in:
        assumes 1 ≡ mainst;
@@ -408,6 +528,30 @@ int opb(void)
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
              mainst;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns SF
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
+     assigns mainst
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, SF,
+             mainst;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
index b46e121b4fa6ad880d696c82e8a7fe7914b08467..59019d29de575c9d3c002abce06057b5d09f7361 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
@@ -32,6 +32,33 @@ int rr = 1;
      ensures aorai_CurOperation ≡ op_opa;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
              S7;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, r;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, r;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, r;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, r;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, r;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, r;
+     assigns S5
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, r;
+     assigns S6
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, r;
+     assigns S7
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, r;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -108,6 +135,33 @@ int rr = 1;
      ensures aorai_CurOperation ≡ op_opa;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
              S7;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, res;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, res;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, res;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, res;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, res;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, res;
+     assigns S5
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, res;
+     assigns S6
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, res;
+     assigns S7
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7, res;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -208,6 +262,33 @@ int opa(int r)
      ensures aorai_CurOperation ≡ op_opb;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
              S7;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S5
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S6
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S7
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -281,6 +362,33 @@ int opa(int r)
      ensures aorai_CurOperation ≡ op_opb;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
              S7;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S5
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S6
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S7
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -374,6 +482,33 @@ void opb(void)
      ensures aorai_CurOperation ≡ op_opc;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
              S7;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S5
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S6
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S7
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -440,6 +575,33 @@ void opb(void)
      ensures aorai_CurOperation ≡ op_opc;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
              S7;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S5
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S6
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S7
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -542,6 +704,33 @@ void opc(void)
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
              S7;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S5
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S6
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S7
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -615,6 +804,33 @@ void opc(void)
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
              S7;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S2
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S3
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S4
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S5
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S6
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
+     assigns S7
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, S3, S4, S5, S6,
+             S7;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
index f767063f9aa1402a8fbf71fc38437edeca2c5631..1431fa716c3b4d91756d07526ea2c633f1174e1f 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
@@ -24,6 +24,16 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_isPresent;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
      
      behavior buch_state_End_out:
        ensures 0 ≡ End;
@@ -67,6 +77,16 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_isPresent;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
      
      behavior buch_state_End_in:
        assumes 1 ≡ Idle ∧ res ≢ -1;
@@ -174,6 +194,16 @@ int isPresent(int *t, int max, int val)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_foo;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
      
      behavior buch_state_End_in:
        assumes 1 ≡ WillDoFoo;
@@ -216,6 +246,16 @@ int isPresent(int *t, int max, int val)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_foo;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
      
      behavior buch_state_End_in:
        assumes 1 ≡ End;
@@ -271,6 +311,16 @@ void foo(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
      
      behavior buch_state_End_out:
        ensures 0 ≡ End;
@@ -313,6 +363,16 @@ void foo(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
      
      behavior buch_state_End_in:
        assumes 1 ≡ End;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
index 20877ef3efbc682ae9945697a51710eb5053b9bf..56ba35bfc725a9e244a5be663abe9017446ccff9 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -20,6 +20,14 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_decode_int;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns main_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
      
      behavior buch_state_S1_in:
        assumes 1 ≡ S1;
@@ -62,6 +70,14 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_decode_int;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns main_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
      
      behavior buch_state_S1_in:
        assumes 1 ≡ S1;
@@ -189,6 +205,14 @@ int decode_int(char *s)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_factorial;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns main_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
      
      behavior buch_state_S1_out:
        ensures 0 ≡ S1;
@@ -233,6 +257,14 @@ int decode_int(char *s)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_factorial;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns main_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
      
      behavior buch_state_S1_in:
        assumes 1 ≡ S2 ∨ 1 ≡ S1;
@@ -311,6 +343,14 @@ int factorial(int value)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns main_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
      
      behavior buch_state_S1_in:
        assumes 1 ≡ main_0;
@@ -353,6 +393,14 @@ int factorial(int value)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S1 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns S2 \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
+     assigns main_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
      
      behavior buch_state_S1_in:
        assumes 1 ≡ S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
index 1bdb8e21ade640879e4bc42e998cf9a9c2f14b91..8c9faad26773d78513719836e6856f9cfd4abbb8 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -21,6 +21,16 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_isPresent;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
      
      behavior buch_state_End_out:
        ensures 0 ≡ End;
@@ -66,6 +76,16 @@ enum aorai_OpStatusList {
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_isPresent;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo, res;
      
      behavior buch_state_End_in:
        assumes (1 ≡ Idle ∧ res ≢ -1) ∨ (1 ≡ End ∧ res ≢ -1);
@@ -180,6 +200,16 @@ int isPresent(int *t, int size, int val)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_foo;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
      
      behavior buch_state_End_in:
        assumes 1 ≡ WillDoFoo;
@@ -222,6 +252,16 @@ int isPresent(int *t, int size, int val)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_foo;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
      
      behavior buch_state_End_in:
        assumes 1 ≡ End;
@@ -277,6 +317,16 @@ void foo(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
      
      behavior buch_state_End_out:
        ensures 0 ≡ End;
@@ -319,6 +369,16 @@ void foo(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, WillDoFoo;
      
      behavior buch_state_End_in:
        assumes 1 ≡ End;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
index c6931e9735d88722e6f14510cac10c63293b66a9..c7e017d08d504c11ddbf2c410794c4ab96b2c667 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
@@ -28,6 +28,24 @@ enum aorai_OpStatusList {
      ensures aorai_CurOperation ≡ op_isPresentRec;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
              WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns IgnoreFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
      
      behavior buch_state_End_out:
        ensures 0 ≡ End;
@@ -82,6 +100,24 @@ enum aorai_OpStatusList {
      ensures aorai_CurOperation ≡ op_isPresentRec;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
              WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
+     assigns IgnoreFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
      
      behavior buch_state_End_out:
        ensures 0 ≡ End;
@@ -206,6 +242,24 @@ int isPresentRec(int *t, int i, int max, int val)
      ensures aorai_CurOperation ≡ op_isPresent;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
              WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns IgnoreFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
      
      behavior buch_state_End_out:
        ensures 0 ≡ End;
@@ -259,6 +313,24 @@ int isPresentRec(int *t, int i, int max, int val)
      ensures aorai_CurOperation ≡ op_isPresent;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
              WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
+     assigns IgnoreFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo, res;
      
      behavior buch_state_End_in:
        assumes 1 ≡ IgnoreFoo ∧ res ≢ -1;
@@ -348,6 +420,24 @@ int isPresent(int *t, int max, int val)
      ensures aorai_CurOperation ≡ op_foo;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
              WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns IgnoreFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
      
      behavior buch_state_End_in:
        assumes 1 ≡ WillDoFoo;
@@ -399,6 +489,24 @@ int isPresent(int *t, int max, int val)
      ensures aorai_CurOperation ≡ op_foo;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
              WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns IgnoreFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
      
      behavior buch_state_End_in:
        assumes 1 ≡ End;
@@ -464,6 +572,24 @@ void foo(void)
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
              WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns IgnoreFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
      
      behavior buch_state_End_out:
        ensures 0 ≡ End;
@@ -515,6 +641,24 @@ void foo(void)
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
              WillDoFoo;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns End
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns Idle
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns IgnoreFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
+     assigns WillDoFoo
+       \from aorai_CurOpStatus, aorai_CurOperation, End, Idle, IgnoreFoo,
+             WillDoFoo;
      
      behavior buch_state_End_in:
        assumes 1 ≡ End;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
index dd49304a1587042373367e110f6a2776659f54e6..541b2c925a348a01a2ed36158f45f14207a5d55a 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
@@ -25,6 +25,14 @@ int myAge = 0;
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_increment;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, main_0;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns main_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
      
      behavior buch_state_S1_in:
        assumes 1 ≡ S1 ∧ nobody.Age ≡ 1;
@@ -63,6 +71,14 @@ int myAge = 0;
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_increment;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, main_0;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns main_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
      
      behavior buch_state_S1_in:
        assumes 1 ≡ S1 ∧ nobody.Age ≡ 1;
@@ -118,6 +134,14 @@ void increment(void)
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, main_0;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns main_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
      
      behavior buch_state_S1_in:
        assumes 1 ≡ main_0 ∧ nobody.Age ≡ 0;
@@ -156,6 +180,14 @@ void increment(void)
      ensures aorai_CurOpStatus ≡ aorai_Terminated;
      ensures aorai_CurOperation ≡ op_main;
      assigns aorai_CurOpStatus, aorai_CurOperation, S1, main_0;
+     assigns aorai_CurOpStatus
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns aorai_CurOperation
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns S1
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
+     assigns main_0
+       \from aorai_CurOpStatus, aorai_CurOperation, S1, main_0, nobody.Age;
      
      behavior buch_state_S1_in:
        assumes 1 ≡ S1 ∧ nobody.Age ≡ 1;
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
index 3a6d4d2a8b0618d67ccd678b53713208d7e14939..c2f8fbb2a856b5c40f721d8f5e954bc866eb988c 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing declared_function.i (no preprocessing)
 [kernel] Parsing TMPDIR/aorai_declared_function_0_prove.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0_prove.i:105: Warning: 
+[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0_prove.i:112: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
index 9978b066020d6e29a93eb1d579a286b6d5fcbebe..58a818caca436713b5e74afea334c63764e435be 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
@@ -2,5 +2,5 @@
 [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
 [kernel] Parsing TMPDIR/aorai_incorrect_0_prove.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0_prove.i:70: Warning: 
+[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0_prove.i:77: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
index 80915856615d80692afbea34a939455e0bb02bf8..60bf5507e20a07373d1b73e4c8a8e960c38decbd 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing serial.c (with preprocessing)
 [kernel] Parsing TMPDIR/aorai_serial_0_prove.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0_prove.i:1273: Warning: 
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0_prove.i:1291: Warning: 
   Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype