Merge branch 'cherry-pick-bfb3dbbd' into '23.2'

Merging of W123-017 into 23.2

See merge request eng/spark/why3!11

src/gnat/gnat_main.ml

@@ -232,9 +232,23 @@ let report_messages c obj =
         | Some pa -> Some (Session_itp.get_proof_attempt_parent s pa)
       in
       let extra_info =
+        let default = { Gnat_expl.pretty_node = None; inlined = None } in
         match unproved_goal with
-        | None -> { Gnat_expl.pretty_node = None; inlined = None }
-        | Some g -> Gnat_objectives.get_extra_info g
+        | None -> default
+        | Some g ->
+            (* In some cases (CE goals in replay) the goal might not be
+               properly registered. In that case, we attempt to find a parent
+               goal that is registered. *)
+            try
+              Gnat_objectives.get_extra_info g
+            with Not_found ->
+              if C.is_ce_goal s g then
+                match Session_itp.get_proof_parent s g with
+                | Session_itp.Theory _ -> default
+                | Session_itp.Trans t ->
+                  try Gnat_objectives.get_extra_info (Session_itp.get_trans_parent s t)
+                  with Not_found -> default
+              else { Gnat_expl.pretty_node = None; inlined = None }
       in
       Gnat_report.Not_Proved (extra_info, model, manual_info) in
   Gnat_report.register obj (C.Save_VCs.check_to_json s obj) result

src/gnat/gnat_objectives.ml

@@ -22,7 +22,7 @@ type status =
 module GoalCmp = struct
    (* module to provide comparison goals *)
   type t = goal_id
-  let compare a b = Pervasives.compare a b
+  let compare a b = Stdlib.compare a b
 end
 
 module GoalMap = Session_itp.Hpn
@@ -1069,20 +1069,21 @@ let session_find_ce_pa c obj =
 
 exception Found_goal_id of Session_itp.proofNodeID
 
+let is_ce_goal s g =
+  match parent_transform_name s g with
+  | Some tr when tr = ce_transform -> true
+  | _ -> false
+
 let session_find_unproved_goal c obj =
 
   let obj_rec = Gnat_expl.HCheck.find explmap obj in
   let session = c.Controller_itp.controller_session in
-  let is_ce_goal g =
-    match parent_transform_name session g with
-    | Some tr when tr = ce_transform -> true
-    | _ -> false
-  in
   let traversal_function () g =
     match g with
     | Session_itp.APn g ->
-        if not (Session_itp.pn_proved session g) && (not (is_ce_goal g)) then
-          raise (Found_goal_id g)
+        if not (Session_itp.pn_proved session g)
+           && (not (is_ce_goal session g))
+        then raise (Found_goal_id g)
     | _ -> () in
 
   let iter_on_sub_goal g =
@@ -1189,4 +1190,6 @@ let (_: unit) = C.register_observer (fun x y z ->
   if x = 0 && y = 0 && z = 0 then
     raise Exit)
 
+
+
 end

src/gnat/gnat_objectives.mli

@@ -178,6 +178,7 @@ val all_split_leaf_goals : unit -> unit
 
 val goal_has_splits : Session_itp.session -> goal_id -> bool
 
+val is_ce_goal : Session_itp.session -> Session_itp.proofNodeID -> bool
 val is_valid_not_ce: Session_itp.session -> Session_itp.proofNodeID -> bool
 
 val session_proved_status : Controller_itp.controller -> objective -> bool