diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 08dff72aecdaf42f1a9270efab1c75ed5bcc4fa1..9a375909b533a24d259fd6ffe46d216995d2436e 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -421,18 +421,22 @@ let neg_trans kf trans =
           ([stop],[]) l
       in
       let cond =
-        List.fold_left
-          (fun cond stop ->
-             let trans = Path_analysis.get_edges start stop auto in
-             List.fold_left
-               (fun cond tr ->
-                  Logic_simplification.tand
-                    cond (Logic_simplification.tnot tr.cross))
-               cond trans)
-          TTrue same_start
+        if Data_for_aorai.isObservableFunction kf then begin
+          let cond =
+            List.fold_left
+              (fun cond stop ->
+                 let trans = Path_analysis.get_edges start stop auto in
+                 List.fold_left
+                   (fun cond tr ->
+                      Logic_simplification.tand
+                        cond (Logic_simplification.tnot tr.cross))
+                   cond trans)
+              TTrue same_start
+          in
+          let cond = fst (Logic_simplification.simplifyCond cond) in
+          Aorai_utils.crosscond_to_pred cond kf Promelaast.Call
+        end else Logic_const.pfalse
       in
-      let cond = fst (Logic_simplification.simplifyCond cond) in
-      let cond = Aorai_utils.crosscond_to_pred cond kf Promelaast.Call in
       let cond =
         Logic_const.por (Aorai_utils.is_out_of_state_pred start, cond)
       in
diff --git a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
index ffb2b1dba40beac39e7d8ae3ef6327438b971a0b..393c8d852246b8489296d98a3f7c5c4cd06b4753 100644
--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -170,12 +170,14 @@ void f(void)
       ensures 0 ≡ aorai_intermediate_state;
     
     behavior Buchi_behavior_out_1:
+      assumes 0 ≡ aorai_intermediate_state_0;
       ensures 0 ≡ aorai_intermediate_state_0;
     
     behavior Buchi_behavior_out_2:
       ensures 0 ≡ final;
     
     behavior Buchi_behavior_out_3:
+      assumes 0 ≡ first_step;
       ensures 0 ≡ first_step;
     
     behavior Buchi_behavior_out_4: