Commit 673b1c10 authored by MARCHE Claude's avatar MARCHE Claude

fix again broken session

parent c60e4dcc
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../tree_of_list.mlw" proved="true">
<theory name="TreeOfList" proved="true">
......@@ -24,7 +24,7 @@
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC tree_of_list_aux.5" expl="precondition" proved="true">
<proof prover="3" timelimit="1"><result status="valid" time="0.01" steps="36"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="36"/></proof>
</goal>
<goal name="VC tree_of_list_aux.6" expl="postcondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="l&#39;1">
......@@ -39,7 +39,6 @@
</transf>
</goal>
<goal name="VC tree_of_list" expl="VC for tree_of_list" proved="true">
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
......
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