updated proof session

parent 95b8d69d
......@@ -222,7 +222,7 @@ module InPlaceRevSeq
returns { (s1,s2) -> s == s1 ++ cons x s2 }
=
if s[i] = x then (s[0 .. i], s[i+1 ..])
else begin assert { mem x s[i+1 .. ] }; mem_decomp x s (i+1) end
else begin (* assert { mem x s[i+1 .. ] }; *) mem_decomp x s (i+1) end
type loc
......
......@@ -5,8 +5,8 @@
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="1" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" steplimit="1" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.0" timelimit="6" steplimit="-1" memlimit="1000"/>
<file name="../linked_list_rev.mlw" expanded="true">
<prover id="6" name="Z3" version="4.4.0" timelimit="16" steplimit="-1" memlimit="1000"/>
<file name="../linked_list_rev.mlw">
<theory name="Disjoint" sum="d9538770c8f60c61e92f6baffbf62d5d">
<goal name="WP_parameter mem_decomp" expl="VC for mem_decomp">
<proof prover="3" timelimit="5"><result status="valid" time="0.02" steps="48"/></proof>
......@@ -133,25 +133,22 @@
</transf>
</goal>
</theory>
<theory name="InPlaceRevSeq" sum="0a10ca60a59ee46a4a887c84c46c2cd4">
<theory name="InPlaceRevSeq" sum="103490a816b50361aa8269515016ce5f">
<goal name="WP_parameter mem_decomp" expl="VC for mem_decomp">
<transf name="split_goal_wp">
<goal name="WP_parameter mem_decomp.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.02" steps="61"/></proof>
</goal>
<goal name="WP_parameter mem_decomp.2" expl="2. assertion">
<proof prover="5" timelimit="30" steplimit="-1"><result status="valid" time="8.39"/></proof>
<goal name="WP_parameter mem_decomp.2" expl="2. variant decrease">
<proof prover="3"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="WP_parameter mem_decomp.3" expl="3. variant decrease">
<proof prover="3"><result status="valid" time="0.01" steps="5"/></proof>
<goal name="WP_parameter mem_decomp.3" expl="3. precondition">
<proof prover="3"><result status="valid" time="0.04" steps="15"/></proof>
</goal>
<goal name="WP_parameter mem_decomp.4" expl="4. precondition">
<proof prover="3"><result status="valid" time="0.04" steps="22"/></proof>
<proof prover="6"><result status="valid" time="11.65"/></proof>
</goal>
<goal name="WP_parameter mem_decomp.5" expl="5. precondition">
<proof prover="3" steplimit="-1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter mem_decomp.6" expl="6. postcondition">
<goal name="WP_parameter mem_decomp.5" expl="5. postcondition">
<proof prover="3"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
</transf>
......@@ -173,11 +170,11 @@
</goal>
<goal name="WP_parameter list_seg_functional.3" expl="3. precondition">
<proof prover="3" steplimit="-1"><result status="valid" time="0.15" steps="258"/></proof>
<proof prover="6" timelimit="5" steplimit="1"><result status="valid" time="1.10"/></proof>
<proof prover="6" timelimit="5" steplimit="1"><result status="timeout" time="4.97"/></proof>
</goal>
<goal name="WP_parameter list_seg_functional.4" expl="4. precondition">
<proof prover="3" steplimit="-1"><result status="valid" time="0.16" steps="262"/></proof>
<proof prover="6" timelimit="5" steplimit="1"><result status="valid" time="0.20"/></proof>
<proof prover="6" timelimit="5" steplimit="1"><result status="valid" time="4.69"/></proof>
</goal>
<goal name="WP_parameter list_seg_functional.5" expl="5. postcondition">
<proof prover="5"><result status="valid" time="0.02"/></proof>
......@@ -221,15 +218,11 @@
<proof prover="5" timelimit="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter list_seg_append.4" expl="4. postcondition">
<transf name="simplify_trivial_quantification">
<goal name="WP_parameter list_seg_append.4.1" expl="1. postcondition">
<proof prover="6"><result status="valid" time="1.06"/></proof>
</goal>
</transf>
<proof prover="6"><result status="valid" time="2.52"/></proof>
</goal>
<goal name="WP_parameter list_seg_append.5" expl="5. postcondition">
<proof prover="3" steplimit="-1"><result status="valid" time="0.09" steps="147"/></proof>
<proof prover="5" timelimit="6"><result status="valid" time="1.63"/></proof>
<proof prover="5" timelimit="6"><result status="valid" time="0.48"/></proof>
</goal>
</transf>
</goal>
......@@ -251,7 +244,7 @@
<proof prover="3"><result status="valid" time="0.05" steps="60"/></proof>
</goal>
<goal name="WP_parameter list_seg_prefix.5" expl="5. postcondition">
<proof prover="6"><result status="valid" time="4.31"/></proof>
<proof prover="5" timelimit="16" steplimit="-1"><result status="valid" time="7.54"/></proof>
</goal>
<goal name="WP_parameter list_seg_prefix.6" expl="6. postcondition">
<proof prover="3"><result status="valid" time="0.98" steps="744"/></proof>
......@@ -379,7 +372,7 @@
<proof prover="3"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter app.11" expl="11. loop invariant preservation">
<proof prover="6"><result status="valid" time="4.30"/></proof>
<proof prover="5" timelimit="16" steplimit="-1"><result status="valid" time="3.93"/></proof>
</goal>
<goal name="WP_parameter app.12" expl="12. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02" steps="16"/></proof>
......@@ -394,7 +387,7 @@
<proof prover="3"><result status="valid" time="0.09" steps="123"/></proof>
</goal>
<goal name="WP_parameter app.13.1.1.2" expl="2. VC for app">
<proof prover="5"><result status="valid" time="5.63"/></proof>
<proof prover="5"><result status="valid" time="3.42"/></proof>
</goal>
</transf>
</goal>
......@@ -403,7 +396,7 @@
</transf>
</goal>
<goal name="WP_parameter app.14" expl="14. loop invariant preservation">
<proof prover="6"><result status="valid" time="4.77"/></proof>
<proof prover="5" timelimit="16" steplimit="-1"><result status="valid" time="3.65"/></proof>
</goal>
<goal name="WP_parameter app.15" expl="15. loop variant decrease">
<proof prover="3"><result status="valid" time="0.85" steps="346"/></proof>
......@@ -414,18 +407,18 @@
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter app.17" expl="17. assertion">
<proof prover="3"><result status="valid" time="0.09" steps="109"/></proof>
<proof prover="3"><result status="valid" time="0.21" steps="109"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter app.18" expl="18. assertion">
<proof prover="3"><result status="valid" time="1.73" steps="580"/></proof>
<proof prover="5"><result status="valid" time="1.52"/></proof>
<proof prover="3"><result status="valid" time="1.73" steps="613"/></proof>
<proof prover="5"><result status="valid" time="0.69"/></proof>
</goal>
<goal name="WP_parameter app.19" expl="19. assertion">
<proof prover="5"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter app.20" expl="20. postcondition">
<proof prover="6"><result status="valid" time="4.08"/></proof>
<proof prover="6" timelimit="6"><result status="valid" time="5.99"/></proof>
</goal>
</transf>
</goal>
......@@ -453,22 +446,22 @@
<proof prover="3" steplimit="-1"><result status="valid" time="0.20" steps="187"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.8" expl="8. loop invariant preservation">
<proof prover="3" steplimit="-1"><result status="valid" time="2.84" steps="1235"/></proof>
<proof prover="3" steplimit="-1"><result status="valid" time="2.84" steps="1231"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.9" expl="9. loop invariant preservation">
<proof prover="6"><result status="valid" time="5.13"/></proof>
<proof prover="6" timelimit="6"><result status="valid" time="5.13"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.10" expl="10. loop invariant preservation">
<proof prover="6"><result status="valid" time="1.72"/></proof>
<proof prover="5" timelimit="16" steplimit="-1"><result status="valid" time="1.40"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.11" expl="11. loop invariant preservation">
<proof prover="6"><result status="valid" time="5.97"/></proof>
<proof prover="6"><result status="valid" time="10.27"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.12" expl="12. loop variant decrease">
<proof prover="3" steplimit="-1"><result status="valid" time="0.41" steps="253"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.13" expl="13. postcondition">
<proof prover="3" steplimit="-1"><result status="valid" time="0.43" steps="1066"/></proof>
<proof prover="3" steplimit="-1"><result status="valid" time="0.43" steps="993"/></proof>
</goal>
</transf>
</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