Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 2b45658a authored by MARCHE Claude's avatar MARCHE Claude
Browse files

fix sessions for nightly replay

parent c266cbf3
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
examples/mergesort_queue/why3session.xml
+ 18
− 117
View file @ 2b45658a
...@@ -2,265 +2,188 @@ ...@@ -2,265 +2,188 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="5" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="8" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.6" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="1.20.prv" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.30" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../mergesort_queue.mlw" expanded="true"> <file name="../mergesort_queue.mlw" expanded="true">
<theory name="MergesortQueue" sum="3c38c1216cfab92b40972e70acecfeff" expanded="true"> <theory name="MergesortQueue" sum="3c38c1216cfab92b40972e70acecfeff" expanded="true">
<goal name="Transitive.Trans" expl=""> <goal name="Transitive.Trans" expl="">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="5"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof>
</goal> </goal>
<goal name="WP_parameter merge" expl="VC for merge"> <goal name="WP_parameter merge" expl="VC for merge">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter merge.1" expl="loop invariant init"> <goal name="WP_parameter merge.1" expl="loop invariant init">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="4"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="5"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.2" expl="loop invariant init"> <goal name="WP_parameter merge.2" expl="loop invariant init">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="9"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.3" expl="loop invariant init"> <goal name="WP_parameter merge.3" expl="loop invariant init">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="9"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.4" expl="loop invariant init"> <goal name="WP_parameter merge.4" expl="loop invariant init">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="7"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="7"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.5" expl="precondition"> <goal name="WP_parameter merge.5" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="10"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.6" expl="loop invariant preservation"> <goal name="WP_parameter merge.6" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="14"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="10"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.7" expl="loop invariant preservation"> <goal name="WP_parameter merge.7" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="5"><result status="valid" time="0.00" steps="10"/></proof> <proof prover="5"><result status="valid" time="0.00" steps="10"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.8" expl="loop invariant preservation"> <goal name="WP_parameter merge.8" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="5"><result status="valid" time="0.00" steps="10"/></proof> <proof prover="5"><result status="valid" time="0.00" steps="10"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.9" expl="loop invariant preservation"> <goal name="WP_parameter merge.9" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="1" timelimit="10" memlimit="0" obsolete="true"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="10"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.10" expl="loop variant decrease"> <goal name="WP_parameter merge.10" expl="loop variant decrease">
<proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="14"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="10"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.11" expl="precondition"> <goal name="WP_parameter merge.11" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="13"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="13"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.12" expl="loop invariant preservation"> <goal name="WP_parameter merge.12" expl="loop invariant preservation">
<proof prover="2" obsolete="true"><result status="valid" time="0.22"/></proof> <proof prover="5"><result status="valid" time="1.05" steps="2499"/></proof>
<proof prover="5"><result status="valid" time="1.05" steps="2937"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.13" expl="loop invariant preservation"> <goal name="WP_parameter merge.13" expl="loop invariant preservation">
<proof prover="2" obsolete="true"><result status="valid" time="0.08"/></proof> <proof prover="5"><result status="valid" time="0.13" steps="518"/></proof>
<proof prover="5"><result status="valid" time="0.13" steps="416"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.14" expl="loop invariant preservation"> <goal name="WP_parameter merge.14" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.12" steps="123"/></proof> <proof prover="5"><result status="valid" time="0.03" steps="82"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="83"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.15" expl="loop invariant preservation"> <goal name="WP_parameter merge.15" expl="loop invariant preservation">
<proof prover="1" timelimit="5" obsolete="true"><result status="valid" time="0.09"/></proof>
<proof prover="5"><result status="valid" time="0.17" steps="277"/></proof> <proof prover="5"><result status="valid" time="0.17" steps="277"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.16" expl="loop variant decrease"> <goal name="WP_parameter merge.16" expl="loop variant decrease">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="21"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="21"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.17" expl="precondition"> <goal name="WP_parameter merge.17" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="13"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="13"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.18" expl="precondition"> <goal name="WP_parameter merge.18" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="16"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="16"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.19" expl="precondition"> <goal name="WP_parameter merge.19" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="19"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="19"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.20" expl="loop invariant preservation"> <goal name="WP_parameter merge.20" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="44"/></proof>
<proof prover="5"><result status="valid" time="0.97" steps="2701"/></proof> <proof prover="5"><result status="valid" time="0.97" steps="2701"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.21" expl="loop invariant preservation"> <goal name="WP_parameter merge.21" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="43"/></proof> <proof prover="5"><result status="valid" time="0.15" steps="787"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.15" steps="805"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.22" expl="loop invariant preservation"> <goal name="WP_parameter merge.22" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.04" steps="43"/></proof> <proof prover="8"><result status="valid" time="0.13"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="timeout" time="2.00"/></proof>
<proof prover="6"><result status="valid" time="0.21"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.23" expl="loop invariant preservation"> <goal name="WP_parameter merge.23" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.06" steps="145"/></proof>
<proof prover="1" timelimit="10" memlimit="0" obsolete="true"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.28" steps="308"/></proof> <proof prover="5"><result status="valid" time="0.28" steps="308"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.24" expl="loop variant decrease"> <goal name="WP_parameter merge.24" expl="loop variant decrease">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="40"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="73"/></proof> <proof prover="5"><result status="valid" time="0.02" steps="73"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.25" expl="precondition"> <goal name="WP_parameter merge.25" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="19"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="19"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.26" expl="loop invariant preservation"> <goal name="WP_parameter merge.26" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="44"/></proof> <proof prover="5"><result status="valid" time="0.90" steps="2989"/></proof>
<proof prover="5"><result status="valid" time="1.16" steps="3073"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.27" expl="loop invariant preservation"> <goal name="WP_parameter merge.27" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="43"/></proof> <proof prover="8"><result status="valid" time="0.14"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="timeout" time="2.00"/></proof>
<proof prover="6"><result status="valid" time="0.22"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.28" expl="loop invariant preservation"> <goal name="WP_parameter merge.28" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="43"/></proof> <proof prover="5"><result status="valid" time="0.15" steps="791"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.15" steps="787"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.29" expl="loop invariant preservation"> <goal name="WP_parameter merge.29" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.10" steps="147"/></proof> <proof prover="8" timelimit="10" memlimit="4000"><result status="valid" time="1.02"/></proof>
<proof prover="2" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
<proof prover="5"><result status="timeout" time="2.00"/></proof>
<proof prover="6" timelimit="10" memlimit="4000"><result status="valid" time="1.22"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.30" expl="loop variant decrease"> <goal name="WP_parameter merge.30" expl="loop variant decrease">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="41"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="74"/></proof> <proof prover="5"><result status="valid" time="0.03" steps="74"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.31" expl="precondition"> <goal name="WP_parameter merge.31" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="5"><result status="valid" time="0.00" steps="13"/></proof> <proof prover="5"><result status="valid" time="0.00" steps="13"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.32" expl="loop invariant preservation"> <goal name="WP_parameter merge.32" expl="loop invariant preservation">
<proof prover="2" obsolete="true"><result status="valid" time="0.24"/></proof> <proof prover="5"><result status="valid" time="1.02" steps="3336"/></proof>
<proof prover="5"><result status="valid" time="1.26" steps="3333"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.33" expl="loop invariant preservation"> <goal name="WP_parameter merge.33" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.14" steps="128"/></proof> <proof prover="5"><result status="valid" time="0.03" steps="83"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="84"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.34" expl="loop invariant preservation"> <goal name="WP_parameter merge.34" expl="loop invariant preservation">
<proof prover="2" obsolete="true"><result status="valid" time="0.07"/></proof> <proof prover="5"><result status="valid" time="0.12" steps="531"/></proof>
<proof prover="5"><result status="valid" time="0.12" steps="415"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.35" expl="loop invariant preservation"> <goal name="WP_parameter merge.35" expl="loop invariant preservation">
<proof prover="1" timelimit="5" obsolete="true"><result status="valid" time="1.03"/></proof>
<proof prover="5"><result status="valid" time="0.16" steps="277"/></proof> <proof prover="5"><result status="valid" time="0.16" steps="277"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.36" expl="loop variant decrease"> <goal name="WP_parameter merge.36" expl="loop variant decrease">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="36"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="21"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="21"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.37" expl="precondition"> <goal name="WP_parameter merge.37" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="5"><result status="valid" time="0.00" steps="12"/></proof> <proof prover="5"><result status="valid" time="0.00" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.38" expl="loop invariant preservation"> <goal name="WP_parameter merge.38" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="12"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.39" expl="loop invariant preservation"> <goal name="WP_parameter merge.39" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="12"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.40" expl="loop invariant preservation"> <goal name="WP_parameter merge.40" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="12"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.41" expl="loop invariant preservation"> <goal name="WP_parameter merge.41" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="1" timelimit="10" memlimit="0" obsolete="true"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.00" steps="12"/></proof> <proof prover="5"><result status="valid" time="0.00" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.42" expl="loop variant decrease"> <goal name="WP_parameter merge.42" expl="loop variant decrease">
<proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="36"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="12"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.43" expl="precondition"> <goal name="WP_parameter merge.43" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="14"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="14"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.44" expl="precondition"> <goal name="WP_parameter merge.44" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="17"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="17"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.45" expl="precondition"> <goal name="WP_parameter merge.45" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="20"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="20"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.46" expl="loop invariant preservation"> <goal name="WP_parameter merge.46" expl="loop invariant preservation">
<proof prover="2" obsolete="true"><result status="valid" time="0.22"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="26"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="26"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.47" expl="loop invariant preservation"> <goal name="WP_parameter merge.47" expl="loop invariant preservation">
<proof prover="2" obsolete="true"><result status="valid" time="0.08"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="29"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="29"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.48" expl="loop invariant preservation"> <goal name="WP_parameter merge.48" expl="loop invariant preservation">
<proof prover="1" obsolete="true"><result status="valid" time="2.52"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="29"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="29"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.49" expl="loop invariant preservation"> <goal name="WP_parameter merge.49" expl="loop invariant preservation">
<proof prover="1" timelimit="5" obsolete="true"><result status="valid" time="0.19"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="50"/></proof> <proof prover="5"><result status="valid" time="0.02" steps="50"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.50" expl="loop variant decrease"> <goal name="WP_parameter merge.50" expl="loop variant decrease">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="59"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="27"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="27"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.51" expl="precondition"> <goal name="WP_parameter merge.51" expl="precondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="20"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="20"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.52" expl="loop invariant preservation"> <goal name="WP_parameter merge.52" expl="loop invariant preservation">
<proof prover="2" obsolete="true"><result status="valid" time="0.26"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="26"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="26"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.53" expl="loop invariant preservation"> <goal name="WP_parameter merge.53" expl="loop invariant preservation">
<proof prover="1" obsolete="true"><result status="valid" time="2.29"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="29"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="29"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.54" expl="loop invariant preservation"> <goal name="WP_parameter merge.54" expl="loop invariant preservation">
<proof prover="2" obsolete="true"><result status="valid" time="0.09"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="29"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="29"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.55" expl="loop invariant preservation"> <goal name="WP_parameter merge.55" expl="loop invariant preservation">
<proof prover="3" edited="mergesort_queue_MergesortQueue_WP_parameter_merge_3.v" obsolete="true"><result status="valid" time="0.26"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="50"/></proof> <proof prover="5"><result status="valid" time="0.02" steps="50"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.56" expl="loop variant decrease"> <goal name="WP_parameter merge.56" expl="loop variant decrease">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="58"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="28"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="28"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.57" expl="postcondition"> <goal name="WP_parameter merge.57" expl="postcondition">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="5"><result status="valid" time="0.00" steps="11"/></proof> <proof prover="5"><result status="valid" time="0.00" steps="11"/></proof>
</goal> </goal>
<goal name="WP_parameter merge.58" expl="postcondition"> <goal name="WP_parameter merge.58" expl="postcondition">
<proof prover="1" timelimit="5" obsolete="true"><result status="valid" time="0.07"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="75"/></proof> <proof prover="5"><result status="valid" time="0.04" steps="75"/></proof>
</goal> </goal>
</transf> </transf>
...@@ -268,85 +191,63 @@ ...@@ -268,85 +191,63 @@
<goal name="WP_parameter mergesort" expl="VC for mergesort" expanded="true"> <goal name="WP_parameter mergesort" expl="VC for mergesort" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter mergesort.1" expl="loop invariant init"> <goal name="WP_parameter mergesort.1" expl="loop invariant init">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.07" steps="53"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="26"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="26"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.2" expl="loop invariant init"> <goal name="WP_parameter mergesort.2" expl="loop invariant init">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="4"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="5"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.3" expl="precondition"> <goal name="WP_parameter mergesort.3" expl="precondition">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="7"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="8"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="8"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.4" expl="precondition"> <goal name="WP_parameter mergesort.4" expl="precondition">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="14"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="14"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.5" expl="loop invariant preservation" expanded="true"> <goal name="WP_parameter mergesort.5" expl="loop invariant preservation" expanded="true">
<proof prover="2" timelimit="30"><result status="valid" time="3.59"/></proof> <proof prover="2"><result status="valid" time="2.76"/></proof>
<proof prover="6" timelimit="10" memlimit="4000"><result status="valid" time="8.52"/></proof> <proof prover="8" timelimit="10" memlimit="4000"><result status="valid" time="5.89"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.6" expl="loop invariant preservation"> <goal name="WP_parameter mergesort.6" expl="loop invariant preservation">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.06" steps="76"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="71"/></proof> <proof prover="5"><result status="valid" time="0.03" steps="71"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.7" expl="loop variant decrease"> <goal name="WP_parameter mergesort.7" expl="loop variant decrease">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="27"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="26"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="26"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.8" expl="loop invariant preservation"> <goal name="WP_parameter mergesort.8" expl="loop invariant preservation">
<proof prover="1" obsolete="true"><result status="valid" time="0.13"/></proof>
<proof prover="5"><result status="valid" time="0.29" steps="226"/></proof> <proof prover="5"><result status="valid" time="0.29" steps="226"/></proof>
<proof prover="7" obsolete="true"><result status="valid" time="0.23"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.9" expl="loop invariant preservation"> <goal name="WP_parameter mergesort.9" expl="loop invariant preservation">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.06" steps="29"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="56"/></proof> <proof prover="5"><result status="valid" time="0.02" steps="56"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.10" expl="loop variant decrease"> <goal name="WP_parameter mergesort.10" expl="loop variant decrease">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="16"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="16"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.11" expl="assertion"> <goal name="WP_parameter mergesort.11" expl="assertion">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="7"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="8"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="8"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.12" expl="assertion"> <goal name="WP_parameter mergesort.12" expl="assertion">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.03" steps="48"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="21"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="21"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.13" expl="variant decrease"> <goal name="WP_parameter mergesort.13" expl="variant decrease">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.03" steps="45"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="60"/></proof> <proof prover="5"><result status="valid" time="0.02" steps="60"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.14" expl="variant decrease"> <goal name="WP_parameter mergesort.14" expl="variant decrease">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.04" steps="49"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="64"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="64"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.15" expl="precondition"> <goal name="WP_parameter mergesort.15" expl="precondition">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="12"/></proof>
<proof prover="5"><result status="valid" time="0.00" steps="13"/></proof> <proof prover="5"><result status="valid" time="0.00" steps="13"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.16" expl="postcondition"> <goal name="WP_parameter mergesort.16" expl="postcondition">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.39" steps="353"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="104"/></proof> <proof prover="5"><result status="valid" time="0.05" steps="104"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.17" expl="assertion"> <goal name="WP_parameter mergesort.17" expl="assertion">
<proof prover="1" obsolete="true"><result status="valid" time="0.08"/></proof> <proof prover="8"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="unknown" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.10"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.18" expl="postcondition"> <goal name="WP_parameter mergesort.18" expl="postcondition">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter mergesort.18.1" expl="VC for mergesort"> <goal name="WP_parameter mergesort.18.1" expl="VC for mergesort">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="4"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="5"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof>
</goal> </goal>
<goal name="WP_parameter mergesort.18.2" expl="VC for mergesort"> <goal name="WP_parameter mergesort.18.2" expl="VC for mergesort">
<proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="3"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
</goal> </goal>
</transf> </transf>
......
examples/tests-provers/bv/why3session.xml
+ 11
− 14
View file @ 2b45658a
...@@ -9,7 +9,7 @@ ...@@ -9,7 +9,7 @@
<prover id="4" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="4" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.01" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="5" name="Alt-Ergo" version="1.01" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bv.why" expanded="true"> <file name="../bv.why" expanded="true">
<theory name="CheckBV64" sum="a69e7936e9b3736b53a1a06d1557d503" expanded="true"> <theory name="CheckBV64" sum="a69e7936e9b3736b53a1a06d1557d503">
<goal name="ok_zero" expl=""> <goal name="ok_zero" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
...@@ -208,19 +208,19 @@ ...@@ -208,19 +208,19 @@
<proof prover="3"><result status="timeout" time="0.92"/></proof> <proof prover="3"><result status="timeout" time="0.92"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
<goal name="smoke6" expl="" expanded="true"> <goal name="smoke6" expl="">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="0.46"/></proof> <proof prover="1"><result status="unknown" time="0.46"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof> <proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
<goal name="smoke7" expl="" expanded="true"> <goal name="smoke7" expl="">
<proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof> <proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
<proof prover="1"><result status="unknown" time="0.51"/></proof> <proof prover="1"><result status="unknown" time="0.51"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof> <proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
<goal name="smoke8" expl="" expanded="true"> <goal name="smoke8" expl="">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="0.44"/></proof> <proof prover="1"><result status="unknown" time="0.44"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof> <proof prover="2"><result status="unknown" time="0.00"/></proof>
...@@ -382,7 +382,7 @@ ...@@ -382,7 +382,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof> <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="CheckBV32" sum="9a0215c8a7245c48b487371f67df8950"> <theory name="CheckBV32" sum="9a0215c8a7245c48b487371f67df8950" expanded="true">
<goal name="ok_zero" expl=""> <goal name="ok_zero" expl="">
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof> <proof prover="1"><result status="valid" time="0.03"/></proof>
...@@ -596,15 +596,14 @@ ...@@ -596,15 +596,14 @@
<proof prover="3"><result status="timeout" time="0.96"/></proof> <proof prover="3"><result status="timeout" time="0.96"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
<goal name="smoke8" expl=""> <goal name="smoke8" expl="" expanded="true">
<proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof> <proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
<proof prover="1"><result status="unknown" time="0.44"/></proof> <proof prover="1"><result status="unknown" time="0.44"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof> <proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="0.92"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="CheckBV16" sum="b944f76414b884563c0502c12ba6dc16"> <theory name="CheckBV16" sum="b944f76414b884563c0502c12ba6dc16" expanded="true">
<goal name="ok_zero" expl=""> <goal name="ok_zero" expl="">
<proof prover="0"><result status="valid" time="0.04" steps="87"/></proof> <proof prover="0"><result status="valid" time="0.04" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof> <proof prover="1"><result status="valid" time="0.04"/></proof>
...@@ -784,7 +783,7 @@ ...@@ -784,7 +783,7 @@
<proof prover="3"><result status="timeout" time="0.96"/></proof> <proof prover="3"><result status="timeout" time="0.96"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
<goal name="smoke3" expl=""> <goal name="smoke3" expl="" expanded="true">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="0.48"/></proof> <proof prover="1"><result status="unknown" time="0.48"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof> <proof prover="2"><result status="unknown" time="0.01"/></proof>
...@@ -818,15 +817,14 @@ ...@@ -818,15 +817,14 @@
<proof prover="3"><result status="timeout" time="0.95"/></proof> <proof prover="3"><result status="timeout" time="0.95"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
<goal name="smoke8" expl=""> <goal name="smoke8" expl="" expanded="true">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="0.43"/></proof> <proof prover="1"><result status="unknown" time="0.43"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof> <proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="0.97"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="CheckBV8" sum="05518dc91aa5666cf77ec6c0d7299767"> <theory name="CheckBV8" sum="05518dc91aa5666cf77ec6c0d7299767" expanded="true">
<goal name="ok_zero" expl=""> <goal name="ok_zero" expl="">
<proof prover="0"><result status="valid" time="0.04" steps="87"/></proof> <proof prover="0"><result status="valid" time="0.04" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof> <proof prover="1"><result status="valid" time="0.05"/></proof>
...@@ -1040,11 +1038,10 @@ ...@@ -1040,11 +1038,10 @@
<proof prover="3"><result status="timeout" time="0.94"/></proof> <proof prover="3"><result status="timeout" time="0.94"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof> <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
<goal name="smoke8" expl=""> <goal name="smoke8" expl="" expanded="true">
<proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof> <proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
<proof prover="1"><result status="unknown" time="0.45"/></proof> <proof prover="1"><result status="unknown" time="0.45"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof> <proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="0.94"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="0.99"/></proof> <proof prover="4" timelimit="1"><result status="timeout" time="0.99"/></proof>
</goal> </goal>
</theory> </theory>
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment