From 927689e2905ad49c1e79c0b162ef863ca0884ef7 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Sun, 26 Dec 2021 11:00:33 +0100
Subject: [PATCH] [aorai] fix initial value of states in presence of
 'observables' directive

---
 src/plugins/aorai/aorai_utils.ml                      | 8 +++++---
 src/plugins/aorai/tests/ya/oracle/observed.res.oracle | 2 +-
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 2c3075fad5b..635ed887209 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 04109b0773f..986a6bd390b 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 ∧
-- 
GitLab