Commit 35d7f859 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

updated proof sessions

parent 1a05fa5f
......@@ -8,43 +8,44 @@
<prover id="3" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../hashtbl_impl.mlw" expanded="true">
<theory name="HashtblImpl" sum="b4b929eee69772640bfb4b31dbef8020" expanded="true">
<theory name="HashtblImpl" sum="eb9f2c9e15846389cacca7c943e63c28" expanded="true">
<goal name="bucket_bounds" expanded="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="16"/></proof>
</goal>
<goal name="WP_parameter create" expl="VC for create" expanded="true">
<proof prover="4"><result status="valid" time="0.14"/></proof>
<proof prover="4"><result status="valid" time="0.14" steps="50"/></proof>
</goal>
<goal name="WP_parameter clear" expl="VC for clear" expanded="true">
<proof prover="4"><result status="valid" time="0.16"/></proof>
<proof prover="4"><result status="valid" time="0.16" steps="71"/></proof>
</goal>
<goal name="WP_parameter resize" expl="VC for resize" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter resize.1" expl="1. array creation size" expanded="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="WP_parameter resize.2" expl="2. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.08"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter resize.3" expl="3. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="58"/></proof>
</goal>
<goal name="WP_parameter resize.4" expl="4. index in array bounds" expanded="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="WP_parameter resize.5" expl="5. index in array bounds" expanded="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.06" steps="9"/></proof>
</goal>
<goal name="WP_parameter resize.6" expl="6. variant decrease" expanded="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="24"/></proof>
</goal>
<goal name="WP_parameter resize.7" expl="7. precondition" expanded="true">
<proof prover="4"><result status="valid" time="0.08"/></proof>
<proof prover="4"><result status="valid" time="0.08" steps="38"/></proof>
</goal>
<goal name="WP_parameter resize.8" expl="8. precondition" expanded="true">
<transf name="inline_all" expanded="true">
<goal name="WP_parameter resize.8.1" expl="1. precondition" expanded="true">
<proof prover="1" timelimit="15"><result status="valid" time="1.38"/></proof>
<proof prover="1" timelimit="15"><result status="valid" time="0.95"/></proof>
</goal>
</transf>
</goal>
......@@ -53,16 +54,16 @@
<goal name="WP_parameter resize.9.1" expl="1. precondition" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter resize.9.1.1" expl="1. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="2" timelimit="15"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter resize.9.1.2" expl="2. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.16"/></proof>
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter resize.9.1.3" expl="3. precondition" expanded="true">
<proof prover="2" timelimit="15"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter resize.9.1.4" expl="4. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter resize.9.1.5" expl="5. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
......@@ -72,35 +73,34 @@
</transf>
</goal>
<goal name="WP_parameter resize.10" expl="10. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.08" steps="17"/></proof>
</goal>
<goal name="WP_parameter resize.11" expl="11. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="35"/></proof>
</goal>
<goal name="WP_parameter resize.12" expl="12. type invariant" expanded="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter resize.13" expl="13. type invariant" expanded="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.05" steps="7"/></proof>
</goal>
<goal name="WP_parameter resize.14" expl="14. type invariant" expanded="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter resize.15" expl="15. type invariant" expanded="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter resize.16" expl="16. loop invariant init" expanded="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.06" steps="22"/></proof>
</goal>
<goal name="WP_parameter resize.17" expl="17. loop invariant init" expanded="true">
<proof prover="4"><result status="valid" time="0.44"/></proof>
<proof prover="4"><result status="valid" time="0.44" steps="98"/></proof>
</goal>
<goal name="WP_parameter resize.18" expl="18. index in array bounds" expanded="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter resize.19" expl="19. type invariant" expanded="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter resize.20" expl="20. precondition" expanded="true">
<transf name="inline_all" expanded="true">
......@@ -110,43 +110,43 @@
</transf>
</goal>
<goal name="WP_parameter resize.21" expl="21. precondition" expanded="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="12"/></proof>
</goal>
<goal name="WP_parameter resize.22" expl="22. precondition" expanded="true">
<transf name="inline_all" expanded="true">
<goal name="WP_parameter resize.22.1" expl="1. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="2.63"/></proof>
<proof prover="4"><result status="valid" time="2.18" steps="178"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter resize.23" expl="23. loop invariant preservation" expanded="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter resize.24" expl="24. loop invariant preservation" expanded="true">
<proof prover="4"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="36"/></proof>
</goal>
<goal name="WP_parameter resize.25" expl="25. type invariant" expanded="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter resize.26" expl="26. type invariant" expanded="true">
<proof prover="4"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="12"/></proof>
</goal>
<goal name="WP_parameter resize.27" expl="27. type invariant" expanded="true">
<proof prover="4"><result status="valid" time="0.14"/></proof>
<proof prover="4"><result status="valid" time="0.14" steps="59"/></proof>
</goal>
<goal name="WP_parameter resize.28" expl="28. type invariant" expanded="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter list_find" expl="VC for list_find" expanded="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="59"/></proof>
</goal>
<goal name="WP_parameter find" expl="VC for find" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter find.1" expl="1. index in array bounds" expanded="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter find.2" expl="2. postcondition" expanded="true">
<proof prover="0" edited="hashtbl_impl_HashtblImpl_WP_parameter_find_1.v"><result status="valid" time="1.10"/></proof>
......@@ -156,19 +156,19 @@
<goal name="WP_parameter list_remove" expl="VC for list_remove" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter list_remove.1" expl="1. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="2"/></proof>
</goal>
<goal name="WP_parameter list_remove.2" expl="2. variant decrease" expanded="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="11"/></proof>
</goal>
<goal name="WP_parameter list_remove.3" expl="3. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.05" steps="16"/></proof>
</goal>
<goal name="WP_parameter list_remove.4" expl="4. variant decrease" expanded="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="11"/></proof>
</goal>
<goal name="WP_parameter list_remove.5" expl="5. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="27"/></proof>
</goal>
</transf>
</goal>
......@@ -177,7 +177,7 @@
<goal name="WP_parameter remove.1" expl="1. index in array bounds" expanded="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="17"/></proof>
</goal>
<goal name="WP_parameter remove.2" expl="2. postcondition" expanded="true">
<proof prover="0" edited="hashtbl_impl_HashtblImpl_WP_parameter_remove_2.v"><result status="valid" time="1.08"/></proof>
......@@ -185,12 +185,12 @@
<goal name="WP_parameter remove.3" expl="3. index in array bounds" expanded="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.06" steps="5"/></proof>
</goal>
<goal name="WP_parameter remove.4" expl="4. type invariant" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="8"/></proof>
</goal>
<goal name="WP_parameter remove.5" expl="5. type invariant" expanded="true">
<transf name="inline_all" expanded="true">
......@@ -202,22 +202,22 @@
<goal name="WP_parameter remove.6" expl="6. type invariant" expanded="true">
<transf name="inline_all" expanded="true">
<goal name="WP_parameter remove.6.1" expl="1. type invariant" expanded="true">
<proof prover="4"><result status="valid" time="0.44"/></proof>
<proof prover="4"><result status="valid" time="0.44" steps="116"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter remove.7" expl="7. type invariant" expanded="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="8"/></proof>
</goal>
<goal name="WP_parameter remove.8" expl="8. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="8"/></proof>
</goal>
<goal name="WP_parameter remove.9" expl="9. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
</transf>
</goal>
......@@ -225,15 +225,15 @@
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter add.1" expl="1. index in array bounds" expanded="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="22"/></proof>
</goal>
<goal name="WP_parameter add.2" expl="2. index in array bounds" expanded="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="7"/></proof>
</goal>
<goal name="WP_parameter add.3" expl="3. type invariant" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="10"/></proof>
</goal>
<goal name="WP_parameter add.4" expl="4. type invariant" expanded="true">
<proof prover="0" edited="hashtbl_impl_HashtblImpl_WP_parameter_add_1.v"><result status="valid" time="2.08"/></proof>
......@@ -254,12 +254,12 @@
</goal>
<goal name="WP_parameter add.6" expl="6. type invariant" expanded="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="10"/></proof>
</goal>
<goal name="WP_parameter add.7" expl="7. postcondition" expanded="true">
<transf name="inline_all" expanded="true">
<goal name="WP_parameter add.7.1" expl="1. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="7"/></proof>
</goal>
</transf>
</goal>
......@@ -269,7 +269,7 @@
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter add.8.1.1" expl="1. postcondition" expanded="true">
<proof prover="1" timelimit="20"><result status="valid" time="0.08"/></proof>
<proof prover="4"><result status="valid" time="0.13"/></proof>
<proof prover="4"><result status="valid" time="0.13" steps="9"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
......@@ -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="79590f88b910b806d8e4109777ab8ee7" expanded="true">
<theory name="DancingLinks" sum="31e47d22027d383b35ca03167e1467ab" 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">
......
......@@ -11,41 +11,41 @@
<goal name="WP_parameter set_zeros" expl="VC for set_zeros">
<transf name="split_goal_wp">
<goal name="WP_parameter set_zeros.1" expl="1. postcondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter set_zeros.2" expl="2. loop invariant init">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter set_zeros.3" expl="3. type invariant">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="WP_parameter set_zeros.4" expl="4. index in array bounds">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="WP_parameter set_zeros.5" expl="5. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter set_zeros.6" expl="6. type invariant">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter set_zeros.7" expl="7. postcondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter harness" expl="VC for harness">
<transf name="split_goal_wp">
<goal name="WP_parameter harness.1" expl="1. array creation size">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
<goal name="WP_parameter harness.2" expl="2. assertion">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="AllZeros" sum="791471af260f297a97e7cb2b0aadbc4e" expanded="true">
<theory name="AllZeros" sum="1d320632b50748c7da056f42e9fe27a9" expanded="true">
<goal name="WP_parameter all_zeros1" expl="VC for all_zeros1" expanded="true">
<proof prover="3"><result status="valid" time="0.02" steps="104"/></proof>
</goal>
......@@ -56,7 +56,7 @@
<proof prover="3"><result status="valid" time="0.01" steps="42"/></proof>
</goal>
<goal name="WP_parameter all_zeros4" expl="VC for all_zeros4" expanded="true">
<proof prover="3"><result status="valid" time="0.02" steps="52"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="50"/></proof>
</goal>
</theory>
</file>
......
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