From a21665e58fb828f351c4a3877014bbce7c8abd76 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 2 Sep 2025 14:13:20 +0200 Subject: [PATCH] OCaml 5 memory blowup workaround This commits try to workaround a memory blowup in Why3 by changing the `space_overhead` configuration of the GC before calling SMT solvers. This hack should be removed once the root cause has been found and fixed. Time impact is limited (< 1%). --- src/ecSmt.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/ecSmt.ml b/src/ecSmt.ml index 22fdd196a..84943dc4b 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -1724,7 +1724,15 @@ let check ?notify (pi : P.prover_infos) (hyps : LDecl.hyps) (concl : form) = Format.eprintf "dumping in %s" filename; let filename = Printf.sprintf "%.4d-%s" tkid filename in out_task filename task)); - let (tp, res) = EcUtils.timed (P.execute_task ?notify pi) task in + let (tp, res) = EcUtils.timed (fun task -> + if Sys.ocaml_release.major = 5 then begin + let control = Gc.get () in + Gc.set { control with space_overhead = min 20 control.space_overhead; }; + EcUtils.try_finally + (fun () -> P.execute_task ?notify pi task) + (fun () -> Gc.set control) + end else P.execute_task ?notify pi task + ) task in if 1 <= pi.P.pr_verbose then notify |> oiter (fun notify -> notify `Warning (lazy (