Avoid to index subgoals when not needed.

engine.ml

@@ -18,8 +18,9 @@ type task = {
   (* Original goal name. *)
   goalname: string;
   (* Subgoal identifier.
-     Typically a goal is translated to multiple subgoals by a solver. *)
-  subgoal: int;
+     Typically a goal is translated to multiple subgoals by a solver.
+     [None] means the goal has no subgoals. *)
+  subgoal: int option;
   (* The formula to verify. *)
   formula: string;
   (* Verification result.
@@ -70,6 +71,20 @@ let check_compatibility solver model =
 
 let tasks_of_property solver { axioms; goals } =
   let module S = (val solver: Solver.S) in
+  let make_task goalname subgoal formula =
+    let id =
+      Format.sprintf "%s%s"
+        goalname
+        (Option.value_map subgoal
+           ~default:""
+           ~f:(fun idx -> Format.sprintf ".%d" idx))
+    in
+    { id;
+      goalname;
+      subgoal;
+      formula = Format.asprintf "%a" S.pretty formula;
+      result = None; }
+  in
   let hypothesis =
     match axioms with
     | [] ->
@@ -86,14 +101,9 @@ let tasks_of_property solver { axioms; goals } =
     ~f:(fun { name; formula; } ->
         let elts = S.(repr (translate ~hypothesis ~goal:formula)) in
         let tasks =
-          List.mapi
-            elts
-            ~f:(fun idx elt ->
-                { id = Format.sprintf "%s.%d" name idx;
-                  goalname = name;
-                  subgoal = idx;
-                  formula = Format.asprintf "%a" S.pretty elt;
-                  result = None; })
+          if List.length elts = 1
+          then [ make_task name None (List.hd_exn elts) ]
+          else List.mapi elts ~f:(fun idx elt -> make_task name (Some idx) elt)
         in
         Hashtbl.set table ~key:name ~data:tasks);
   table
@@ -174,8 +184,13 @@ let exec_tasks ~raw_options solver config model tasks_htbl =
           tasks
           ~f:(fun task ->
               Logs.app (fun m ->
-                  m "Verifying goal `%s', subgoal %d (%s)."
-                    task.goalname task.subgoal task.id);
+                  m "Verifying goal `%s'%s."
+                    task.goalname
+                    (Option.value_map task.subgoal
+                       ~default:""
+                       ~f:(fun subgoal ->
+                           Format.sprintf ", subgoal %d (%s)"
+                             subgoal task.id)));
               let res_exec_task =
                 (* Build the required command-line. *)
                 build_command ~raw_options solver config model task
@@ -190,7 +205,7 @@ let exec_tasks ~raw_options solver config model tasks_htbl =
                   else begin
                     (* Extract and pretty-print verification result. *)
                     let result = extract_result solver ~log ~output in
-                    Logs.app (fun m -> m "Result %s: %a."
+                    Logs.app (fun m -> m "Result of `%s': %a."
                                  task.id Solver.Result.pretty result);
                     Sys.remove output;
                     if Solver.Result.equal result Solver.Result.Failure