Commit 4d5bffd3 authored by MARCHE Claude's avatar MARCHE Claude

fixed pb with PVS 'proveit' heap size

parent 0b005fe5
......@@ -164,7 +164,7 @@ Scheduled for 31 october 2013
* new versions of provers:
** Alt-Ergo 0.95.2
** CVC4 1.1 (& 1.2 ?)
** CVC4 1.1 & 1.2
** Coq 8.4pl2
** gappa 1.0.0
** SPASS 3.8ds
......
......@@ -175,7 +175,7 @@
edited="genealogy_Genealogy_Child_is_son_or_daughter_1.pvs"
obsolete="false"
archived="false">
<result status="highfailure" time="0.00"/>
<result status="valid" time="0.89"/>
</proof>
<proof
prover="10"
......
......@@ -432,7 +432,8 @@ version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
version_ok = "6.0"
version_bad = "^[0-5]\..+$"
command = "%l/why3-cpulimit 0 %m -s %l/why3-call-pvs %l proveit -f %f"
# not why3-cpulimit 0 %m because 'proveit' allocates 8Gb at start-up
command = "%l/why3-cpulimit 0 0 -s %l/why3-call-pvs %l proveit -f %f"
driver = "drivers/pvs.drv"
in_place = true
editor = "pvs"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment