From bbe2eaa15433fa881d23cb0e43577e84f9222fcd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 3 Oct 2024 11:11:44 +0200 Subject: [PATCH] Catch Step_limit_reached consistently with Timeout This is a partial fix for #1244 that only addresses the fatal error issue, but not incrementality. --- src/lib/frontend/frontend.ml | 1 + src/lib/reasoners/satml_frontend.ml | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index d2d437024..c730a88d5 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -523,6 +523,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct or to increase your timeouts. \ Returned unknown reason = %a@]" Sat_solver_sig.pp_ae_unknown_reason_opt ur; + Fmt.pf ppf "()" | Some model -> Models.pp ppf model diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 2200a8e0a..c0b448983 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1165,6 +1165,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct with | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) | Util.Timeout -> i_dont_know env (Timeout ProofSearch) + | Util.Step_limit_reached n -> i_dont_know env (Step_limit n) | Satml.Sat -> try do_case_split env Util.BeforeMatching; @@ -1205,6 +1206,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct with | Util.Timeout -> i_dont_know env (Timeout ProofSearch) + | Util.Step_limit_reached n -> i_dont_know env (Step_limit n) | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) | Ex.Inconsistent (expl, _cls) -> (*may be raised during matching or CS*) begin @@ -1214,6 +1216,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct with | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) | Util.Timeout -> i_dont_know env (Timeout ProofSearch) + | Util.Step_limit_reached n -> i_dont_know env (Step_limit n) end let rec unsat_rec_prem env ~first_call : unit =