diff --git a/src/plugins/aorai/tests/ya/oracle/seq_unlimited.err.oracle b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0c4ab2b08ea4b83aa87fba82f547006cea3d37e9
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
@@ -0,0 +1,326 @@
+[kernel] Parsing seq_unlimited.i (no preprocessing)
+[aorai] seq_unlimited.i:21: Warning: 
+  Call to find does not follow automaton's specification. This path is assumed to be dead
+[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
+[aorai] seq_unlimited.i:23: Warning: 
+  Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
+[kernel] Parsing TMPDIR/aorai_seq_unlimited_0.i (no preprocessing)
+/* Generated by Frama-C */
+enum aorai_States {
+    aorai_intermediate_state = 0,
+    aorai_reject = 1,
+    b = 2,
+    c = 3,
+    fst = 4
+};
+enum aorai_ListOper {
+    op_find = 2,
+    op_init = 1,
+    op_main = 0
+};
+enum aorai_OpStatusList {
+    aorai_Terminated = 1,
+    aorai_Called = 0
+};
+/*@ check lemma fst_deterministic_trans{L}: \true;
+ */
+/*@ check lemma c_deterministic_trans{L}: \true;
+ */
+/*@ check lemma b_deterministic_trans{L}: \true;
+ */
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
+ */
+/*@ check lemma aorai_intermediate_state_deterministic_trans{L}: \true;
+ */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
+/*@ ghost int aorai_CurStates = fst; */
+/*@ ghost
+  /@ requires aorai_CurStates ≡ b;
+     ensures aorai_CurOpStatus ≡ aorai_Called;
+     ensures aorai_CurOperation ≡ op_init;
+     assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     
+     behavior buch_state_aorai_intermediate_state_in:
+       assumes aorai_CurStates ≡ b;
+       ensures aorai_CurStates ≡ aorai_intermediate_state;
+     
+     behavior buch_state_aorai_intermediate_state_out:
+       assumes aorai_CurStates ≢ b;
+       ensures aorai_CurStates ≢ aorai_intermediate_state;
+     
+     behavior buch_state_aorai_reject_out:
+       ensures aorai_CurStates ≢ aorai_reject;
+     
+     behavior buch_state_b_out:
+       ensures aorai_CurStates ≢ b;
+     
+     behavior buch_state_c_out:
+       ensures aorai_CurStates ≢ c;
+     
+     behavior buch_state_fst_out:
+       ensures aorai_CurStates ≢ fst;
+   @/
+  void init_pre_func(int *a, int n)
+  {
+    /@ slevel full; @/
+    aorai_CurOpStatus = aorai_Called;
+    aorai_CurOperation = op_init;
+    if (2 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state;
+    else aorai_CurStates = aorai_reject;
+    return;
+  }
+
+*/
+
+/*@ ghost
+  /@ requires aorai_CurStates ≡ aorai_intermediate_state;
+     ensures aorai_CurOpStatus ≡ aorai_Terminated;
+     ensures aorai_CurOperation ≡ op_init;
+     assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     
+     behavior buch_state_aorai_intermediate_state_out:
+       ensures aorai_CurStates ≢ aorai_intermediate_state;
+     
+     behavior buch_state_aorai_reject_out:
+       ensures aorai_CurStates ≢ aorai_reject;
+     
+     behavior buch_state_b_out:
+       ensures aorai_CurStates ≢ b;
+     
+     behavior buch_state_c_in:
+       assumes aorai_CurStates ≡ aorai_intermediate_state;
+       ensures aorai_CurStates ≡ c;
+     
+     behavior buch_state_c_out:
+       assumes aorai_CurStates ≢ aorai_intermediate_state;
+       ensures aorai_CurStates ≢ c;
+     
+     behavior buch_state_fst_out:
+       ensures aorai_CurStates ≢ fst;
+   @/
+  void init_post_func(void)
+  {
+    /@ slevel full; @/
+    aorai_CurOpStatus = aorai_Terminated;
+    aorai_CurOperation = op_init;
+    if (0 == aorai_CurStates) aorai_CurStates = c;
+    else aorai_CurStates = aorai_reject;
+    return;
+  }
+
+*/
+
+/*@ requires aorai_CurStates ≡ b;
+    
+    behavior Buchi_property_behavior:
+      ensures aorai_CurStates ≡ c;
+ */
+void init(int *a, int n)
+{
+  /*@ ghost int aorai_Loop_Init_2; */
+  /*@ ghost init_pre_func(a,n); */
+  int i = 0;
+  /*@ ghost aorai_Loop_Init_2 = 1; */
+  aorai_loop_2:
+  /*@ loop invariant Aorai: aorai_CurStates ≡ aorai_intermediate_state;
+      loop invariant Aorai: aorai_CurStates ≢ aorai_reject;
+      loop invariant Aorai: aorai_CurStates ≢ b;
+      loop invariant Aorai: aorai_CurStates ≢ c;
+      loop invariant Aorai: aorai_CurStates ≢ fst;
+  */
+  while (i < n) {
+    /*@ ghost aorai_Loop_Init_2 = 0; */
+    *(a + i) = i;
+    i ++;
+  }
+  /*@ ghost init_post_func(); */
+  return;
+}
+
+/*@ ghost
+  /@ requires \false;
+     ensures aorai_CurOpStatus ≡ aorai_Called;
+     ensures aorai_CurOperation ≡ op_find;
+     assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     
+     behavior buch_state_aorai_intermediate_state_out:
+       ensures aorai_CurStates ≢ aorai_intermediate_state;
+     
+     behavior buch_state_aorai_reject_out:
+       ensures aorai_CurStates ≢ aorai_reject;
+     
+     behavior buch_state_b_out:
+       ensures aorai_CurStates ≢ b;
+     
+     behavior buch_state_c_out:
+       ensures aorai_CurStates ≢ c;
+     
+     behavior buch_state_fst_out:
+       ensures aorai_CurStates ≢ fst;
+   @/
+  void find_pre_func(int *a, int n, int k)
+  {
+    /@ slevel full; @/
+    aorai_CurOpStatus = aorai_Called;
+    aorai_CurOperation = op_find;
+    aorai_CurStates = aorai_reject;
+    return;
+  }
+
+*/
+
+/*@ ghost
+  /@ requires \false;
+     ensures aorai_CurOpStatus ≡ aorai_Terminated;
+     ensures aorai_CurOperation ≡ op_find;
+     assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     
+     behavior buch_state_aorai_intermediate_state_out:
+       ensures aorai_CurStates ≢ aorai_intermediate_state;
+     
+     behavior buch_state_aorai_reject_out:
+       ensures aorai_CurStates ≢ aorai_reject;
+     
+     behavior buch_state_b_out:
+       ensures aorai_CurStates ≢ b;
+     
+     behavior buch_state_c_out:
+       ensures aorai_CurStates ≢ c;
+     
+     behavior buch_state_fst_out:
+       ensures aorai_CurStates ≢ fst;
+   @/
+  void find_post_func(int res)
+  {
+    /@ slevel full; @/
+    aorai_CurOpStatus = aorai_Terminated;
+    aorai_CurOperation = op_find;
+    aorai_CurStates = aorai_reject;
+    return;
+  }
+
+*/
+
+/*@ requires \false; */
+int find(int *a, int n, int k)
+{
+  int __retres;
+  /*@ ghost find_pre_func(a,n,k); */
+  {
+    /*@ ghost int aorai_Loop_Init_12; */
+    int i = 0;
+    /*@ ghost aorai_Loop_Init_12 = 1; */
+    aorai_loop_12:
+    /*@ loop invariant Aorai: aorai_CurStates ≢ aorai_intermediate_state;
+        loop invariant Aorai: aorai_CurStates ≢ aorai_reject;
+        loop invariant Aorai: aorai_CurStates ≢ b;
+        loop invariant Aorai: aorai_CurStates ≢ c;
+        loop invariant Aorai: aorai_CurStates ≢ fst;
+    */
+    while (i < n) {
+      /*@ ghost aorai_Loop_Init_12 = 0; */
+      if (*(a + i) == k) {
+        __retres = i;
+        goto return_label;
+      }
+      i ++;
+    }
+  }
+  __retres = -1;
+  return_label: {
+                  /*@ ghost find_post_func(__retres); */
+                  return __retres;
+                }
+}
+
+/*@ ghost
+  /@ requires \false;
+     ensures aorai_CurOpStatus ≡ aorai_Called;
+     ensures aorai_CurOperation ≡ op_main;
+     assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     
+     behavior buch_state_aorai_intermediate_state_out:
+       ensures aorai_CurStates ≢ aorai_intermediate_state;
+     
+     behavior buch_state_aorai_reject_out:
+       ensures aorai_CurStates ≢ aorai_reject;
+     
+     behavior buch_state_b_out:
+       ensures aorai_CurStates ≢ b;
+     
+     behavior buch_state_c_out:
+       ensures aorai_CurStates ≢ c;
+     
+     behavior buch_state_fst_out:
+       ensures aorai_CurStates ≢ fst;
+   @/
+  void main_pre_func(void)
+  {
+    /@ slevel full; @/
+    aorai_CurOpStatus = aorai_Called;
+    aorai_CurOperation = op_main;
+    aorai_CurStates = aorai_reject;
+    return;
+  }
+
+*/
+
+/*@ ghost
+  /@ requires \false;
+     ensures aorai_CurOpStatus ≡ aorai_Terminated;
+     ensures aorai_CurOperation ≡ op_main;
+     assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+     
+     behavior buch_state_aorai_intermediate_state_out:
+       ensures aorai_CurStates ≢ aorai_intermediate_state;
+     
+     behavior buch_state_aorai_reject_out:
+       ensures aorai_CurStates ≢ aorai_reject;
+     
+     behavior buch_state_b_out:
+       ensures aorai_CurStates ≢ b;
+     
+     behavior buch_state_c_out:
+       ensures aorai_CurStates ≢ c;
+     
+     behavior buch_state_fst_out:
+       ensures aorai_CurStates ≢ fst;
+   @/
+  void main_post_func(int res)
+  {
+    /@ slevel full; @/
+    aorai_CurOpStatus = aorai_Terminated;
+    aorai_CurOperation = op_main;
+    aorai_CurStates = aorai_reject;
+    return;
+  }
+
+*/
+
+/*@ requires \false;
+    
+    behavior aorai_acceptance:
+      ensures \false; */
+int main(void)
+{
+  int __retres;
+  int a[10];
+  int tmp_0;
+  /*@ ghost main_pre_func(); */
+  init(a,10);
+  tmp_0 = find(a,10,5);
+  if (tmp_0) {
+    int tmp;
+    tmp = find(a,10,11);
+    __retres = tmp;
+    goto return_label;
+  }
+  __retres = 0;
+  return_label: {
+                  /*@ ghost main_post_func(__retres); */
+                  return __retres;
+                }
+}
+
+
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.err.oracle b/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..719a33db757f527494e3b1f5cba8a23f679c1c33
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing seq_unlimited.i (no preprocessing)
+[aorai] seq_unlimited.i:21: Warning: 
+  Call to find does not follow automaton's specification. This path is assumed to be dead
+[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
+[aorai] seq_unlimited.i:23: Warning: 
+  Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
+[kernel] Parsing TMPDIR/aorai_seq_unlimited_0_prove.i (no preprocessing)
+[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/seq_unlimited.i b/src/plugins/aorai/tests/ya/seq_unlimited.i
new file mode 100644
index 0000000000000000000000000000000000000000..950ffc1141c8ffe3123ed0b20becdd9a27b3e12c
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/seq_unlimited.i
@@ -0,0 +1,23 @@
+/*run.config*
+  STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance
+*/
+void init(int *a, int n)
+{
+  for(int i = 0; i < n; i++)
+    *(a+i) = i;
+}
+
+int find(int *a, int n, int k)
+{
+  for(int i = 0; i < n; i++)
+    if (a[i] == k) return i;
+  return -1;
+}
+
+int main(void)
+{
+  int a[10];
+  init(a, 10);
+  if (find(a, 10, 5))
+    return find(a, 10, 11);
+}
diff --git a/src/plugins/aorai/tests/ya/seq_unlimited.ya b/src/plugins/aorai/tests/ya/seq_unlimited.ya
new file mode 100644
index 0000000000000000000000000000000000000000..521e5168a94e18d73882e26c8e11338f476faf49
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/seq_unlimited.ya
@@ -0,0 +1,8 @@
+%init: fst;
+%accept: ok;
+%deterministic;
+fst : { CALL(main) } -> b;
+b : { init() } -> c;
+c:  { find()+ } -> ok;
+ok: { RETURN(main) } -> ok;
+