Skip to content

Commit

Permalink
testsuite: regenerate broken sessions
Browse files Browse the repository at this point in the history
  • Loading branch information
@Armael
Armael committed Jun 4, 2024
1 parent e51c182 commit 2bc013c
Show file tree
Hide file tree
Showing 12 changed files with 2,156 additions and 2,005 deletions.
329 changes: 144 additions & 185 deletions creusot/tests/should_succeed/heapsort_generic/why3session.xml
View file

Large diffs are not rendered by default.

Binary file modified creusot/tests/should_succeed/heapsort_generic/why3shapes.gz
View file
Binary file not shown.
256 changes: 116 additions & 140 deletions creusot/tests/should_succeed/hillel/why3session.xml
View file

Large diffs are not rendered by default.

Binary file modified creusot/tests/should_succeed/hillel/why3shapes.gz
View file
Binary file not shown.
265 changes: 142 additions & 123 deletions creusot/tests/should_succeed/knapsack_full/why3session.xml
View file

Large diffs are not rendered by default.

Binary file modified creusot/tests/should_succeed/knapsack_full/why3shapes.gz
View file
Binary file not shown.
350 changes: 175 additions & 175 deletions creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
View file

Large diffs are not rendered by default.

Binary file modified creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz
View file
Binary file not shown.
2,828 changes: 1,512 additions & 1,316 deletions creusot/tests/should_succeed/red_black_tree/why3session.xml
View file

Large diffs are not rendered by default.

Binary file modified creusot/tests/should_succeed/red_black_tree/why3shapes.gz
View file
Binary file not shown.
133 changes: 67 additions & 66 deletions creusot/tests/should_succeed/selection_sort_generic/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,191 +2,192 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"https://www.why3.org/why3session.dtd">
<why3session shape_version="6">
<prover id="1" name="CVC4" version="1.8" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.8" timelimit="30" steplimit="0" memlimit="4000"/>
<prover id="2" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.5.3" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.5.3" timelimit="30" steplimit="0" memlimit="4000"/>
<file format="coma" proved="true">
<path name=".."/><path name="selection_sort_generic.coma"/>
<theory name="SelectionSortGeneric_SelectionSort" proved="true">
<goal name="vc_selection_sort" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_selection_sort.0" expl="type invariant" proved="true">
<proof prover="3"><result status="valid" time="0.016814" steps="12"/></proof>
<proof prover="2"><result status="valid" time="0.033276" steps="13516"/></proof>
</goal>
<goal name="vc_selection_sort.1" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.028910" steps="14"/></proof>
<proof prover="2"><result status="valid" time="0.036769" steps="13748"/></proof>
</goal>
<goal name="vc_selection_sort.2" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.023919" steps="23"/></proof>
<proof prover="2"><result status="valid" time="0.053528" steps="18283"/></proof>
</goal>
<goal name="vc_selection_sort.3" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.020142" steps="18"/></proof>
<proof prover="2"><result status="valid" time="0.040183" steps="17092"/></proof>
</goal>
<goal name="vc_selection_sort.4" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="0.013263" steps="54"/></proof>
<proof prover="2"><result status="valid" time="0.092095" steps="23744"/></proof>
</goal>
<goal name="vc_selection_sort.5" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.077385" steps="23997"/></proof>
<proof prover="2"><result status="valid" time="0.090519" steps="23997"/></proof>
</goal>
<goal name="vc_selection_sort.6" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="0.044965" steps="68"/></proof>
<proof prover="2"><result status="valid" time="0.098681" steps="25616"/></proof>
</goal>
<goal name="vc_selection_sort.7" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="0.103213" steps="32"/></proof>
<proof prover="2"><result status="valid" time="0.090732" steps="22788"/></proof>
</goal>
<goal name="vc_selection_sort.8" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="0.019731" steps="35"/></proof>
<proof prover="2"><result status="valid" time="0.077889" steps="23203"/></proof>
</goal>
<goal name="vc_selection_sort.9" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="0.022211" steps="30"/></proof>
<proof prover="2"><result status="valid" time="0.066482" steps="21472"/></proof>
</goal>
<goal name="vc_selection_sort.10" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.025233" steps="38"/></proof>
<proof prover="2"><result status="valid" time="0.066388" steps="23046"/></proof>
</goal>
<goal name="vc_selection_sort.11" expl="type invariant" proved="true">
<proof prover="3"><result status="valid" time="0.016042" steps="44"/></proof>
<proof prover="2"><result status="valid" time="0.057834" steps="23511"/></proof>
</goal>
<goal name="vc_selection_sort.12" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.018711" steps="52"/></proof>
<proof prover="2"><result status="valid" time="0.065991" steps="24275"/></proof>
</goal>
<goal name="vc_selection_sort.13" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.023220" steps="476"/></proof>
<proof prover="2"><result status="valid" time="0.250464" steps="44769"/></proof>
</goal>
<goal name="vc_selection_sort.14" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.042335" steps="447"/></proof>
<proof prover="2"><result status="valid" time="0.203011" steps="30563"/></proof>
</goal>
<goal name="vc_selection_sort.15" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.021881" steps="53"/></proof>
<proof prover="2"><result status="valid" time="0.071937" steps="23586"/></proof>
</goal>
<goal name="vc_selection_sort.16" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.028795" steps="62"/></proof>
<proof prover="2"><result status="valid" time="0.121278" steps="23608"/></proof>
</goal>
<goal name="vc_selection_sort.17" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.014026" steps="46"/></proof>
<proof prover="2"><result status="valid" time="0.099865" steps="21911"/></proof>
</goal>
<goal name="vc_selection_sort.18" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.158825" steps="23663"/></proof>
<proof prover="2"><result status="valid" time="0.115921" steps="23663"/></proof>
</goal>
<goal name="vc_selection_sort.19" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.103851" steps="30643"/></proof>
<proof prover="2"><result status="valid" time="0.128443" steps="30643"/></proof>
</goal>
<goal name="vc_selection_sort.20" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.074713" steps="27094"/></proof>
<proof prover="2"><result status="valid" time="0.083198" steps="27094"/></proof>
</goal>
<goal name="vc_selection_sort.21" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="0.022203" steps="53"/></proof>
<proof prover="2"><result status="valid" time="0.101666" steps="24758"/></proof>
</goal>
<goal name="vc_selection_sort.22" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.023792" steps="77"/></proof>
<proof prover="2"><result status="valid" time="0.104525" steps="26735"/></proof>
</goal>
<goal name="vc_selection_sort.23" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.026853" steps="85"/></proof>
<proof prover="2"><result status="valid" time="0.114557" steps="26911"/></proof>
</goal>
<goal name="vc_selection_sort.24" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.012713" steps="85"/></proof>
<proof prover="2"><result status="valid" time="0.089692" steps="26916"/></proof>
</goal>
<goal name="vc_selection_sort.25" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.046207" steps="980"/></proof>
<proof prover="2"><result status="valid" time="0.187115" steps="39259"/></proof>
</goal>
<goal name="vc_selection_sort.26" expl="type invariant" proved="true">
<proof prover="3"><result status="valid" time="0.026247" steps="68"/></proof>
<proof prover="2"><result status="valid" time="0.059146" steps="25852"/></proof>
</goal>
<goal name="vc_selection_sort.27" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.021580" steps="93"/></proof>
<proof prover="2"><result status="valid" time="0.147623" steps="27755"/></proof>
</goal>
<goal name="vc_selection_sort.28" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.020003" steps="94"/></proof>
<proof prover="2"><result status="valid" time="0.105383" steps="27760"/></proof>
</goal>
<goal name="vc_selection_sort.29" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.088362" steps="761"/></proof>
<proof prover="2"><result status="valid" time="0.118889" steps="33126"/></proof>
</goal>
<goal name="vc_selection_sort.30" expl="type invariant" proved="true">
<proof prover="3"><result status="valid" time="0.017212" steps="74"/></proof>
<proof prover="2"><result status="valid" time="0.112472" steps="25876"/></proof>
</goal>
<goal name="vc_selection_sort.31" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.017008" steps="76"/></proof>
<proof prover="2"><result status="valid" time="0.064035" steps="25881"/></proof>
</goal>
<goal name="vc_selection_sort.32" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.016863" steps="76"/></proof>
<proof prover="2"><result status="valid" time="0.093281" steps="25882"/></proof>
</goal>
<goal name="vc_selection_sort.33" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.148744" steps="33056"/></proof>
<proof prover="2"><result status="valid" time="0.116944" steps="33056"/></proof>
</goal>
<goal name="vc_selection_sort.34" expl="loop invariant" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_selection_sort.34.0" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.637192" steps="108898"/></proof>
</goal>
</transf>
<proof prover="2"><result status="valid" time="0.404213" steps="60014"/></proof>
</goal>
<goal name="vc_selection_sort.35" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.120032" steps="35248"/></proof>
<proof prover="2"><result status="valid" time="0.209893" steps="35248"/></proof>
</goal>
<goal name="vc_selection_sort.36" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.077750" steps="27937"/></proof>
<proof prover="2"><result status="valid" time="0.157754" steps="27937"/></proof>
</goal>
<goal name="vc_selection_sort.37" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.152069" steps="41657"/></proof>
<proof prover="2"><result status="valid" time="0.282632" steps="41657"/></proof>
</goal>
<goal name="vc_selection_sort.38" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.156921" steps="44470"/></proof>
<proof prover="2"><result status="valid" time="0.255310" steps="44470"/></proof>
</goal>
<goal name="vc_selection_sort.39" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.121469" steps="35237"/></proof>
<proof prover="2"><result status="valid" time="0.244669" steps="35237"/></proof>
</goal>
<goal name="vc_selection_sort.40" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="0.019047" steps="107"/></proof>
<proof prover="2"><result status="valid" time="0.156922" steps="27964"/></proof>
</goal>
<goal name="vc_selection_sort.41" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.026537" steps="96"/></proof>
<proof prover="2"><result status="valid" time="0.082106" steps="27077"/></proof>
</goal>
<goal name="vc_selection_sort.42" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.024579" steps="103"/></proof>
<proof prover="2"><result status="valid" time="0.116554" steps="27229"/></proof>
</goal>
<goal name="vc_selection_sort.43" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.043121" steps="2080"/></proof>
<proof prover="2"><result status="valid" time="0.147056" steps="37945"/></proof>
</goal>
<goal name="vc_selection_sort.44" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.091220" steps="98"/></proof>
<proof prover="2"><result status="valid" time="0.120602" steps="25941"/></proof>
</goal>
<goal name="vc_selection_sort.45" expl="type invariant" proved="true">
<proof prover="3"><result status="valid" time="0.022452" steps="117"/></proof>
<proof prover="2"><result status="valid" time="0.109326" steps="27313"/></proof>
</goal>
<goal name="vc_selection_sort.46" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_selection_sort.46.0" expl="assertion" proved="true">
<transf name="assert" proved="true" arg1="(length1 (inner produced) = length1 (inner produced2) + 1)">
<goal name="vc_selection_sort.46.0.0" expl="asserted formula" proved="true">
<proof prover="3"><result status="valid" time="0.032476" steps="143"/></proof>
</goal>
<goal name="vc_selection_sort.46.0.1" expl="assertion" proved="true">
<proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="2.624028" steps="467480"/></proof>
</goal>
</transf>
<proof prover="1"><result status="valid" time="11.150248" steps="3292948"/></proof>
</goal>
</transf>
</goal>
<goal name="vc_selection_sort.47" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="0.022966" steps="1208"/></proof>
<proof prover="2"><result status="valid" time="0.157366" steps="34967"/></proof>
</goal>
<goal name="vc_selection_sort.48" expl="loop invariant" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_selection_sort.48.0" expl="loop invariant" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="4.408401" steps="1933318"/></proof>
<transf name="inline_goal" proved="true" >
<goal name="vc_selection_sort.48.0.0" expl="loop invariant" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="vc_selection_sort.48.0.0.0" expl="loop invariant" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_selection_sort.48.0.0.0.0" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="9.002549" steps="85989"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="vc_selection_sort.49" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="0.014104" steps="649"/></proof>
<proof prover="2"><result status="valid" time="0.309272" steps="43846"/></proof>
</goal>
<goal name="vc_selection_sort.50" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="0.063948" steps="128"/></proof>
<proof prover="2"><result status="valid" time="0.120471" steps="27390"/></proof>
</goal>
<goal name="vc_selection_sort.51" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.130366" steps="37665"/></proof>
<proof prover="2"><result status="valid" time="0.214283" steps="37665"/></proof>
</goal>
<goal name="vc_selection_sort.52" expl="loop invariant" proved="true">
<proof prover="3"><result status="valid" time="0.016930" steps="135"/></proof>
<proof prover="2"><result status="valid" time="0.144790" steps="29663"/></proof>
</goal>
</transf>
</goal>
Expand Down
Binary file modified creusot/tests/should_succeed/selection_sort_generic/why3shapes.gz
View file
Binary file not shown.

0 comments on commit 2bc013c

Please sign in to comment.