Inform about timeouts.

src/Abduction.ml

@@ -10,9 +10,12 @@ open Aux
 open Joint
 
 let timeout_count = ref 700(* 5000 *)(* 50000 *)
-let fail_timeout_count = ref 5
+let fail_timeout_count = ref 4
 let no_alien_prem = ref (* true *)false
 
+let abd_fail_flag = ref false
+let abd_timeout_flag = ref false
+
 let residuum q prem concl =
   let concl = to_formula concl in
   let res_ty, res_num, res_so =
@@ -581,6 +584,7 @@ let abd_simple q ?without_quant ~bvs ~pms ~dissociate
       "abd_simple: TIMEOUT conflicts with premises skip=%d,@ vs=@ %s;@ ans=@ %a@ --@\n@[<2>%a@ ⟹@ %a@]@\n%!"
       !skip (String.concat "," (List.map var_str vs))
       pr_subst ans pr_subst prem pr_subst concl; *]*)
+    abd_timeout_flag := true;
     None
 
 (* let max_skip = ref 20 *)
@@ -594,6 +598,7 @@ module TermAbd = struct
   type branch = subst * formula * subst
 
   let abd_fail_timeout = !fail_timeout_count
+  let abd_fail_flag = abd_fail_flag
 
   let abd_simple (q, pms, dissociate) ~discard ~validate (bvs, acc) br =
     abd_simple q ~bvs ~pms ~dissociate ~validate ~discard 0 acc br
@@ -616,6 +621,7 @@ module JCA = Joint.JointAbduction (TermAbd)
 let abd_typ q ~bvs ?(dissociate=false) ~validate ~discard brs =
   (*[* Format.printf "abd_typ:@ bvs=@ %a@\n%!"
     pr_vars bvs; *]*)
+  abd_timeout_flag := false;
   let alien_vs = ref [] in
   let alien_eqs = ref [] in
   let rec purge = function

src/Abduction.mli

@@ -16,6 +16,9 @@ val timeout_count : int ref
 val fail_timeout_count : int ref
 val no_alien_prem : bool ref
 
+val abd_fail_flag : bool ref
+val abd_timeout_flag : bool ref
+
 val abd_simple :
   Terms.quant_ops ->
   ?without_quant:unit ->

src/InvarGenT.ml

@@ -100,7 +100,7 @@ let main () =
     "-not_annotating_fun", Arg.Clear Infer.annotating_fun,
     "Do not keep information for annotating `function` nodes";
     "-annotating_letin", Arg.Set Infer.annotating_letin,
-    "Keep information for annotating `function` nodes";
+    "Keep information for annotating `let..in` nodes";
     "-let_in_fallback", Arg.Set let_in_fallback,
     "Annotate `let..in` nodes in fallback mode of .ml generation";
   ] in
@@ -113,7 +113,16 @@ let main () =
       (process_file !fname ~do_sig:!do_sig ~do_ml:!do_ml
          ~verif_ml:!verif_ml ~full_annot:!full_annot)
   with (Report_toplevel _ | Contradiction _) as exn ->
-    pr_exception Format.std_formatter exn; exit 2
+    Format.printf "%a@\n%!" pr_exception exn;
+    if !Abduction.abd_timeout_flag then Format.printf
+        "Perhaps increase the -term_abduction_timeout parameter.@\n%!";
+    if !Abduction.abd_fail_flag then Format.printf
+        "Perhaps increase the -term_abduction_fail parameter.@\n%!";
+    if !NumS.abd_timeout_flag then Format.printf
+        "Perhaps increase the -term_abduction_timeout parameter.@\n%!";
+    if !NumS.abd_fail_flag then Format.printf
+        "Perhaps increase the -term_abduction_fail parameter.@\n%!";
+    exit 2
 
 
 let () =

src/Joint.ml

@@ -16,6 +16,7 @@ module type ABD_PARAMS = sig
   type discarded
   type branch
   val abd_fail_timeout : int
+  val abd_fail_flag : bool ref
   val abd_simple :
     args -> discard:discarded list -> validate:(answer -> unit) ->
     accu -> branch -> accu option
@@ -32,6 +33,7 @@ let debug_dep = ref 0
 module JointAbduction (P : ABD_PARAMS) = struct
 
   let abd args ~discard ~validate init_acc brs =
+    P.abd_fail_flag := false;
     let culprit = ref None
     and best_done = ref (-1) in
     let rec loop fails discard acc done_brs aside_brs = function
@@ -51,7 +53,7 @@ module JointAbduction (P : ABD_PARAMS) = struct
         | Some acc ->
           loop fails discard acc (br::done_brs) aside_brs more_brs
         | None ->
-          if fails >= P.abd_fail_timeout
+          if fails > P.abd_fail_timeout
           then (
             (*[* Format.printf
               "Joint.abd-loop: TIMEOUT %d failed [%d] at@ ans=%a@\n%!"
@@ -60,6 +62,7 @@ module JointAbduction (P : ABD_PARAMS) = struct
             let concl = P.concl_of_br (unsome !culprit) in
             let lc = List.fold_left loc_union dummy_loc
                 (List.map atom_loc concl) in
+            P.abd_fail_flag := true;
             raise (Suspect (concl, lc)));
           loop (fails+1) discard acc done_brs (br::aside_brs) more_brs
 
@@ -76,14 +79,15 @@ module JointAbduction (P : ABD_PARAMS) = struct
           check_aside fails best discard acc (br::done_brs) aside_brs
         | None ->
           if best then culprit := Some br;
-          if P.is_taut (P.extract_ans acc) || fails >= P.abd_fail_timeout
+          if P.is_taut (P.extract_ans acc) || fails > P.abd_fail_timeout
           then (
             (*[* Format.printf
               "abd-check_aside: quit failed [%d] at@ ans=%a@\n%!" ddepth
               P.pr_ans (P.extract_ans acc); *]*)
             let concl = P.concl_of_br (unsome !culprit) in
             let lc = List.fold_left loc_union dummy_loc
                 (List.map atom_loc concl) in
+            if fails > P.abd_fail_timeout then P.abd_fail_flag := true;
             raise (Suspect (concl, lc)))
           else
             loop (fails+1) (P.discard_ans acc::discard) init_acc [] []

src/Joint.mli

@@ -16,6 +16,7 @@ module type ABD_PARAMS = sig
   type discarded
   type branch
   val abd_fail_timeout : int
+  val abd_fail_flag : bool ref
   val abd_simple :
     args -> discard:discarded list -> validate:(answer -> unit) ->
     accu -> branch -> accu option

src/NumS.ml

@@ -14,10 +14,13 @@ let early_num_abduction = ref false(* true *)
 let abd_rotations = ref (* 2 *)3
 let abd_prune_at = ref (* 4 *)6(* 10 *)
 let abd_timeout_count = ref (* 500 *)1000(* 5000 *)(* 50000 *)
-let abd_fail_timeout_count = ref 50
+let abd_fail_timeout_count = ref 10
 let disjelim_rotations = ref 3
 let passing_ineq_trs = ref false
 
+let abd_fail_flag = ref false
+let abd_timeout_flag = ref false
+
 let (!/) i = num_of_int i
 type w = (var_name * num) list * num * loc
 type w_subst = (var_name * w) list
@@ -643,6 +646,7 @@ let abd_simple cmp cmp_w cmp_v uni_v ~bvs ~discard ~validate
   with
   | Contradiction _ -> None
   | Timeout ->
+    abd_timeout_flag := true;
     (*[* Format.printf
       "NumS.abd_simple: TIMEOUT@\neqs_i=@ %a@\nineqs_i=@ %a@\nd_eqn=@ %a@ d_ineqn=@ %a@\nc_eqn=@ %a@\nc_ineqn=@ %a@\n%!"
       pr_w_subst eqs_i pr_ineqs ineqs_i pr_eqn d_eqn pr_ineqn d_ineqn
@@ -673,6 +677,7 @@ module NumAbd = struct
   type branch = (w list * w list) * (w list * w list)
 
   let abd_fail_timeout = !abd_fail_timeout_count
+  let abd_fail_flag = abd_fail_flag
 
   let abd_simple {cmp; cmp_w; cmp_v; uni_v; bvs}
       ~discard ~validate acc br =
@@ -700,6 +705,7 @@ end
 module JCA = Joint.JointAbduction (NumAbd)
 
 let abd q ~bvs ~discard ?(iter_no=2) brs =
+  abd_timeout_flag := false;
   let cmp_v = make_cmp q in
   let cmp (v1,_) (v2,_) = cmp_v v1 v2 in
   let cmp_w (vars1,cst1,_) (vars2,cst2,_) =

src/NumS.mli

@@ -15,6 +15,9 @@ val abd_prune_at : int ref
 val abd_timeout_count : int ref
 val abd_fail_timeout_count : int ref
 val passing_ineq_trs : bool ref
+
+val abd_fail_flag : bool ref
+val abd_timeout_flag : bool ref
 (** For uniformity, return an empty list as introduced
     variables. Raise [Contradiction] if constraints are contradictory
     and [Suspect] if no answer can be found. *)