examples: fixed session files for VerifyThis 2018 solutions

parent 420c347e
......@@ -5,7 +5,7 @@
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../challenge3.mlw" proved="true">
<file name="../verifythis_2018_array_based_queuing_lock_1.mlw" proved="true">
<theory name="Top" proved="true">
<goal name="VC k" expl="VC for k" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
......
......@@ -5,7 +5,7 @@
<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../rougenoir.mlw" proved="true">
<file name="../verifythis_2018_le_rouge_et_le_noir_1.mlw" proved="true">
<theory name="ColoredTiles" proved="true">
<goal name="valid_contr" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="6"/></proof>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../challenge2.mlw" proved="true">
<file name="../verifythis_2018_le_rouge_et_le_noir_2.mlw" proved="true">
<theory name="Top" proved="true">
<goal name="VC bij_preserve" expl="VC for bij_preserve" proved="true">
<transf name="split_goal_wp" proved="true" >
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../challenge1.mlw" proved="true">
<file name="../verifythis_2018_mind_the_gap_1.mlw" proved="true">
<theory name="Top" proved="true">
<goal name="VC any_char" expl="VC for any_char" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
......
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