diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 9d4ddad0f1b44303b0f5732d51266a087ab8eefe..aadd8a359bd7eada4f5cd551479310ebe84c2024 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -398,7 +398,11 @@ let possible_start kf (start,int) =
     Logic_const.por
       (cond, Aorai_utils.crosscond_to_pred tr.cross kf Promelaast.Call)
   in
-  let cond = List.fold_left treat_one_trans Logic_const.pfalse trans in
+  let cond =
+    if Data_for_aorai.isObservableFunction kf then
+      List.fold_left treat_one_trans Logic_const.pfalse trans
+    else Logic_const.ptrue
+  in
   Logic_const.pand (Aorai_utils.is_state_pred start, cond)
 
 let neg_trans kf trans =
diff --git a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
index 986a6bd390bb105f701d9507ede81b34ad319429..4e5eac6d384e44d053a94c743e8c18593fcb8b25 100644
--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -154,11 +154,32 @@ void f(void)
   return;
 }
 
-/*@ behavior Buchi_property_behavior:
-      ensures
-        0 ≡ aorai_intermediate_state ∧
-        0 ≡ aorai_intermediate_state_0 ∧ 0 ≡ final ∧ 0 ≡ init;
+/*@ requires 1 ≡ first_step ∨ 0 ≡ first_step;
+    requires
+      1 ≡ aorai_intermediate_state_0 ∨ 0 ≡ aorai_intermediate_state_0;
+    
+    behavior Buchi_behavior_in_0:
+      assumes 1 ≡ aorai_intermediate_state_0;
+      ensures 1 ≡ aorai_intermediate_state_0;
+    
+    behavior Buchi_behavior_in_1:
+      assumes 1 ≡ first_step;
       ensures 1 ≡ first_step;
+    
+    behavior Buchi_behavior_out_0:
+      ensures 0 ≡ aorai_intermediate_state;
+    
+    behavior Buchi_behavior_out_1:
+      ensures 0 ≡ aorai_intermediate_state_0;
+    
+    behavior Buchi_behavior_out_2:
+      ensures 0 ≡ final;
+    
+    behavior Buchi_behavior_out_3:
+      ensures 0 ≡ first_step;
+    
+    behavior Buchi_behavior_out_4:
+      ensures 0 ≡ init;
  */
 void g(void)
 {
@@ -298,6 +319,8 @@ void g(void)
 void h(void)
 {
   /*@ ghost h_pre_func(); */
+  g();
+  g();
   /*@ ghost h_post_func(); */
   return;
 }