diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 2c3075fad5b7684070d0d6dfff77441ea291ff0f..635ed887209085506d9f8bb7b14a349a81379eab 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -306,9 +306,11 @@ let isCrossableAtInit tr func =
     | TRel(rel,t1,t2) -> eval_rel_at_init rel t1 t2
 
   in
-  match isCross tr.cross with
-  | Bool3.True | Bool3.Undefined -> true
-  | Bool3.False -> false
+  if Data_for_aorai.isObservableFunction func then begin
+    match isCross tr.cross with
+    | Bool3.True | Bool3.Undefined -> true
+    | Bool3.False -> false
+  end else true
 
 (* ************************************************************************* *)
 (** {b Expressions management} *)
diff --git a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
index 04109b0773f7fb092cd277a2173c8b2a57e588bc..986a6bd390bb105f701d9507ede81b34ad319429 100644
--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -15,7 +15,7 @@ enum aorai_OpStatusList {
 /*@ ghost int aorai_intermediate_state_0 = 0; */
 /*@ ghost int final = 0; */
 /*@ ghost int first_step = 0; */
-/*@ ghost int init = 0; */
+/*@ ghost int init = 1; */
 /*@ ghost
   /@ requires
        1 ≡ init ∧ 0 ≡ aorai_intermediate_state ∧