Skip to content

Commit

Permalink
Reactivating timeouts
Browse files Browse the repository at this point in the history
Timeouts were disabled in satml_frontend (check OCamlPro#946); this PR re-enables
them with a generic exception catcher wrapping calls to a possibly invalid
environment.
  • Loading branch information
Stevendeo committed Nov 27, 2023
1 parent f407d75 commit 6f57808
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion src/lib/frontend/frontend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -444,7 +444,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
(* If we have reached an unknown state, we can return it right
away. *)
match SAT.get_unknown_reason env.sat_env with
| Some (Step_limit _) -> raise SAT.I_dont_know
| Some (Step_limit _ | Timeout _) -> raise SAT.I_dont_know
| Some _ ->
(* For now, only the step limit is an unknown step reachable
here. We could raise SAT.I_dont_know as in the previous case,
Expand Down
2 changes: 1 addition & 1 deletion src/lib/reasoners/satml_frontend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1030,7 +1030,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
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
- we raised I_dont_know (legit)
- 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. *)
Expand Down

0 comments on commit 6f57808

Please sign in to comment.