Commit 53768698 authored by MARCHE Claude's avatar MARCHE Claude

updated session with wrong number of steps for Alt-Ergo

parent d1cb56a4
......@@ -16,7 +16,7 @@
<file name="../mergesort_array.mlw" expanded="true">
<theory name="Elt" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Merge" sum="8cf69a18a957f12ca10b0983694178ac" expanded="true">
<theory name="Merge" sum="8cf69a18a957f12ca10b0983694178ac">
<goal name="WP_parameter merge" expl="VC for merge">
<transf name="split_goal_wp">
<goal name="WP_parameter merge.1" expl="1. postcondition">
......@@ -238,7 +238,7 @@
<proof prover="10"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter merge.39" expl="39. loop invariant preservation">
<proof prover="2"><result status="valid" time="1.60" steps="569"/></proof>
<proof prover="2"><result status="valid" time="1.60" steps="593"/></proof>
<proof prover="3"><result status="valid" time="1.64"/></proof>
</goal>
<goal name="WP_parameter merge.40" expl="40. loop invariant preservation">
......@@ -491,7 +491,7 @@
</transf>
</goal>
</theory>
<theory name="TopDownMergesort" sum="84157389ec7e6e31c7815d501480fe11" expanded="true">
<theory name="TopDownMergesort" sum="84157389ec7e6e31c7815d501480fe11">
<goal name="WP_parameter mergesort_rec" expl="VC for mergesort_rec">
<transf name="split_goal_wp">
<goal name="WP_parameter mergesort_rec.1" expl="1. division by zero">
......@@ -590,9 +590,9 @@
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="BottomUpMergesort" sum="a6bce72f8da36cb440dbc9ba0613cd62" expanded="true">
<goal name="WP_parameter bottom_up_mergesort" expl="VC for bottom_up_mergesort" expanded="true">
<transf name="split_goal_wp" expanded="true">
<theory name="BottomUpMergesort" sum="a6bce72f8da36cb440dbc9ba0613cd62">
<goal name="WP_parameter bottom_up_mergesort" expl="VC for bottom_up_mergesort">
<transf name="split_goal_wp">
<goal name="WP_parameter bottom_up_mergesort.1" expl="1. loop invariant init">
<proof prover="2"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
......@@ -622,7 +622,7 @@
<proof prover="8"><result status="valid" time="0.02" steps="15"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter bottom_up_mergesort.6" expl="6. loop invariant init" expanded="true">
<goal name="WP_parameter bottom_up_mergesort.6" expl="6. loop invariant init">
<proof prover="2"><result status="valid" time="0.02" steps="19"/></proof>
<proof prover="8"><result status="valid" time="0.04" steps="20"/></proof>
</goal>
......@@ -852,7 +852,7 @@
</transf>
</goal>
</theory>
<theory name="NaturalMergesort" sum="f5bd8d32ec48878b0768e6bbed72d199" expanded="true">
<theory name="NaturalMergesort" sum="f5bd8d32ec48878b0768e6bbed72d199">
<goal name="WP_parameter find_run" expl="VC for find_run">
<transf name="split_goal_wp">
<goal name="WP_parameter find_run.1" expl="1. loop invariant init">
......@@ -1110,8 +1110,8 @@
<goal name="WP_parameter natural_mergesort.29" expl="29. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.18" steps="267"/></proof>
<proof prover="4"><result status="valid" time="0.37"/></proof>
<proof prover="8"><result status="valid" time="5.30" steps="2275"/></proof>
<proof prover="9"><result status="valid" time="0.50"/></proof>
<proof prover="8"><result status="valid" time="5.30" steps="2461"/></proof>
<proof prover="9"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="WP_parameter natural_mergesort.30" expl="30. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="38"/></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