From 427a1c78b293c1342c5fb6f77903a6a4996066ea Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 8 Nov 2021 13:33:42 +0100
Subject: [PATCH] Push memory limit to 4GB by default.
---
src/verification.ml | 11 ++++++++++-
tests/bin/pyrat.py | 0
2 files changed, 10 insertions(+), 1 deletion(-)
mode change 100644 => 100755 tests/bin/pyrat.py
diff --git a/src/verification.ml b/src/verification.ml
index a8baac2f..fc561e3d 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -11,8 +11,17 @@ let () = Language.register_nnet_support ()
let create_env loadpath =
let config = Autodetection.autodetect ~debug:true () in
- let stdlib = Dirs.Sites.stdlib in
let open Why3 in
+ let config =
+ let main = Whyconf.get_main config in
+ let dft_memlimit = 4000 (* 4 GB *) in
+ let main =
+ Whyconf.(
+ set_limits main (timelimit main) dft_memlimit (running_provers_max main))
+ in
+ Whyconf.set_main config main
+ in
+ let stdlib = Dirs.Sites.stdlib in
( Env.create_env
(loadpath @ stdlib @ Whyconf.loadpath (Whyconf.get_main config)),
config )
diff --git a/tests/bin/pyrat.py b/tests/bin/pyrat.py
old mode 100644
new mode 100755
--
GitLab