Removing model generation when timeout on satml

src/lib/reasoners/sat_solver_sig.ml

@@ -35,19 +35,16 @@ type timeout_reason =
   | Assume
   | ProofSearch
   | ModelGen
-  | ExnRaised of exn
 
 let pp_smt_timeout_reason ppf = function
   | Assume -> Fmt.pf ppf ":assume"
   | ProofSearch -> Fmt.pf ppf ":proof-search"
   | ModelGen -> Fmt.pf ppf ":model-gen"
-  | ExnRaised e -> Fmt.pf ppf "(:failure \"%s\")" (Printexc.to_string e)
 
 let pp_ae_timeout_reason ppf = function
   | Assume -> Fmt.pf ppf "Assume"
   | ProofSearch -> Fmt.pf ppf "ProofSearch"
   | ModelGen -> Fmt.pf ppf "ModelGen"
-  | ExnRaised e -> Fmt.pf ppf "Failure (\"%s\")" (Printexc.to_string e)
 
 type unknown_reason =
   | Incomplete

src/lib/reasoners/sat_solver_sig.mli

@@ -32,7 +32,6 @@ type timeout_reason =
   | Assume
   | ProofSearch
   | ModelGen
-  | ExnRaised of exn
 
 type unknown_reason =
   | Incomplete

src/lib/reasoners/satml_frontend.ml

@@ -1005,41 +1005,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       (* In this case, timeout reason becomes 'ModelGen' *)
       i_dont_know env (Timeout ModelGen)
 
-  (* Tries to generate a model on the environment after the computation was
-     interrupted by a Timeout exception.
-     for that reason, it is impossible to guarantee the environment is sound.
-     A model generated by this function may not be sound at all as well.
-  *)
-  let model_gen_on_timeout env =
-      let i = Options.get_interpretation () in
-      let ti = Options.get_timelimit_interpretation () in
-      if not i || (* not asked to gen a model *)
-         env.model_gen_phase ||  (* we timeouted in model-gen-phase *)
-         Stdlib.(=) ti 0. (* no time allocated for extra model search *)
-      then
-        i_dont_know env (Timeout ProofSearch)
-      else
-        try
-          (* Beware: models generated on timeout of ProofSearch phase may
-             be incoherent wrt. the ground part of the pb (ie. if delta
-             is not empty ? *)
-          env.model_gen_phase <- true;
-          Options.Time.unset_timeout ();
-          Options.Time.set_timeout ti;
-          update_model_and_return_unknown
-            env
-            i
-            ~unknown_reason:(Timeout ProofSearch) (* may becomes ModelGen *)
-        with
-        (* We raised an exception. This can come from four sources:
-           - we raised I_dont_know (legit)
-           - we raised Timeout (Timeout on model generation, legit as weel)
-           - we raised Unsat -> maybe unsound, returning I_dont_know
-           - we broke an invaraiant because the timeout happened during a
-           critical instruction and now the environment is invalid. *)
-        | I_dont_know | Util.Timeout as e -> raise e
-        | e -> i_dont_know env (Timeout (ExnRaised e))
-
   exception Give_up of (E.t * E.t * bool * bool) list
 
   (* Getting [unknown] after a query can mean two things:
@@ -1155,7 +1120,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     try SAT.solve env.satml; assert false
     with
     | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
-    | Util.Timeout -> model_gen_on_timeout env
+    | Util.Timeout -> i_dont_know env (Timeout ProofSearch)
     | Satml.Sat ->
       try
         do_case_split env Util.BeforeMatching;
@@ -1195,7 +1160,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
         unsat_rec env ~first_call:false
 
       with
-      | Util.Timeout -> model_gen_on_timeout env
+      | Util.Timeout -> i_dont_know env (Timeout ProofSearch)
       | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
       | Ex.Inconsistent (expl, _cls) -> (*may be raised during matching or CS*)
         begin
@@ -1204,7 +1169,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
             unsat_rec env ~first_call:false
           with
           | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
-          | Util.Timeout -> model_gen_on_timeout env
+          | Util.Timeout -> i_dont_know env (Timeout ProofSearch)
         end
 
   let rec unsat_rec_prem env ~first_call : unit =