Commit 9d8b9923 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

updated proof sessions

parent 35d7f859
......@@ -6,7 +6,7 @@
<prover id="2" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
<file name="../verifythis_2015_dancing_links.mlw" expanded="true">
<theory name="DancingLinks" sum="31e47d22027d383b35ca03167e1467ab" expanded="true">
<theory name="DancingLinks" sum="03fd71894ffd9889b4cd16510dcdad1f" expanded="true">
<goal name="WP_parameter remove" expl="VC for remove">
<transf name="split_goal_wp">
<goal name="WP_parameter remove.1" expl="1. index in array bounds">
......@@ -74,7 +74,7 @@
<proof prover="3"><result status="valid" time="0.05" steps="35"/></proof>
</goal>
<goal name="WP_parameter put_back.9" expl="9. postcondition">
<proof prover="2"><result status="valid" time="0.54"/></proof>
<proof prover="2"><result status="valid" time="0.38"/></proof>
</goal>
</transf>
</goal>
......
......@@ -822,7 +822,7 @@
</transf>
</goal>
</theory>
<theory name="RingBufferSeq" sum="4f41e9731e19159f10f257068c0e8fcb" expanded="true">
<theory name="RingBufferSeq" sum="d9784ee16c97c4f5e2c2eaf82bce1155" expanded="true">
<goal name="WP_parameter create" expl="VC for create" expanded="true">
<proof prover="5"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
......
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