Skip to content

Commit

Permalink
Update proofs to new why3
Browse files Browse the repository at this point in the history
  • Loading branch information
xldenis committed Oct 25, 2023
1 parent 71e33aa commit b6e36d4
Show file tree
Hide file tree
Showing 170 changed files with 1,719 additions and 1,728 deletions.
4 changes: 2 additions & 2 deletions creusot/tests/should_succeed/100doors/why3session.xml
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="1" name="Z3" version="4.12.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="0" name="Z3" version="4.12.2" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="100doors.mlcfg"/>
<theory name="C100doors_F" proved="true">
<goal name="f&#39;vc" expl="VC for f" proved="true">
<proof prover="1"><result status="valid" time="0.327048" steps="945633"/></proof>
<proof prover="0"><result status="valid" time="0.122415" steps="658174"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified creusot/tests/should_succeed/100doors/why3shapes.gz
Binary file not shown.
4 changes: 2 additions & 2 deletions creusot/tests/should_succeed/all_zero/why3session.xml
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="1" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="all_zero.mlcfg"/>
<theory name="AllZero_AllZero" proved="true">
<goal name="all_zero&#39;vc" expl="VC for all_zero" proved="true">
<proof prover="1"><result status="valid" time="0.038573" steps="808"/></proof>
<proof prover="0"><result status="valid" time="0.038573" steps="806"/></proof>
</goal>
</theory>
</file>
Expand Down
54 changes: 26 additions & 28 deletions creusot/tests/should_succeed/bdd/why3session.xml
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="CVC4" version="1.8" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.5.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.11.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.12.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
Expand All @@ -17,7 +15,7 @@
</theory>
<theory name="Bdd_Impl7_Eq" proved="true">
<goal name="eq&#39;vc" expl="VC for eq" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="808"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.003136" steps="539"/></proof>
</goal>
</theory>
<theory name="Bdd_Impl14_Eq" proved="true">
Expand All @@ -27,7 +25,7 @@
</theory>
<theory name="Bdd_Impl0_Clone" proved="true">
<goal name="clone&#39;&#39;vc" expl="VC for clone&#39;" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="641"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.002978" steps="427"/></proof>
</goal>
</theory>
<theory name="Bdd_Impl15_Clone" proved="true">
Expand All @@ -42,12 +40,12 @@
</theory>
<theory name="Bdd_Impl2_Hash" proved="true">
<goal name="hash&#39;vc" expl="VC for hash" proved="true">
<proof prover="0"><result status="valid" time="0.020000" steps="761"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.003323" steps="513"/></proof>
</goal>
</theory>
<theory name="Bdd_Impl8_Size_Impl" proved="true">
<goal name="size&#39;vc" expl="VC for size" proved="true">
<proof prover="0"><result status="valid" time="0.020000" steps="1203"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.005392" steps="905"/></proof>
</goal>
</theory>
<theory name="Bdd_Impl10_GrowsIsValidBdd_Impl" proved="true">
Expand Down Expand Up @@ -537,7 +535,7 @@
<proof prover="6"><result status="valid" time="0.085307" steps="5854"/></proof>
</goal>
<goal name="and&#39;vc.29" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.067880" steps="258665"/></proof>
<proof prover="4"><result status="valid" time="0.067819" steps="251609"/></proof>
</goal>
<goal name="and&#39;vc.30" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.091440" steps="8389"/></proof>
Expand All @@ -551,13 +549,13 @@
<goal name="and&#39;vc.31.0.0.0" expl="precondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="and&#39;vc.31.0.0.0.0" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.084472" steps="395875"/></proof>
<proof prover="4"><result status="valid" time="0.112833" steps="544049"/></proof>
</goal>
<goal name="and&#39;vc.31.0.0.0.1" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.209960" steps="532284"/></proof>
<proof prover="4"><result status="valid" time="0.050164" steps="216783"/></proof>
</goal>
<goal name="and&#39;vc.31.0.0.0.2" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.104813" steps="458944"/></proof>
<proof prover="4"><result status="valid" time="0.101796" steps="451427"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -575,10 +573,10 @@
<proof prover="6"><result status="valid" time="0.252434" steps="42233"/></proof>
</goal>
<goal name="and&#39;vc.31.1.0.0.1" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.086875" steps="396721"/></proof>
<proof prover="4"><result status="valid" time="0.064557" steps="280230"/></proof>
</goal>
<goal name="and&#39;vc.31.1.0.0.2" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.120648" steps="541351"/></proof>
<proof prover="4"><result status="valid" time="0.109090" steps="462414"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -589,7 +587,7 @@
</transf>
</goal>
<goal name="and&#39;vc.32" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.116839" steps="146074"/></proof>
<proof prover="4"><result status="valid" time="0.034477" steps="140173"/></proof>
</goal>
<goal name="and&#39;vc.33" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.029470" steps="43"/></proof>
Expand Down Expand Up @@ -666,10 +664,10 @@
</transf>
</goal>
<goal name="and&#39;vc.37" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.148957" steps="549303"/></proof>
<proof prover="4"><result status="valid" time="0.160674" steps="533439"/></proof>
</goal>
<goal name="and&#39;vc.38" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.211103" steps="1215556"/></proof>
<proof prover="4"><result status="valid" time="0.073766" steps="268860"/></proof>
</goal>
<goal name="and&#39;vc.39" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
Expand All @@ -681,10 +679,10 @@
<goal name="and&#39;vc.39.0.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="and&#39;vc.39.0.1.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.041714" steps="199045"/></proof>
<proof prover="4"><result status="valid" time="0.045110" steps="188866"/></proof>
</goal>
<goal name="and&#39;vc.39.0.1.1" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.192811" steps="822121"/></proof>
<proof prover="4"><result status="valid" time="0.127787" steps="511952"/></proof>
</goal>
<goal name="and&#39;vc.39.0.1.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.057312" steps="80"/></proof>
Expand All @@ -696,15 +694,15 @@
<goal name="and&#39;vc.39.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="and&#39;vc.39.1.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.034327" steps="178213"/></proof>
<proof prover="4"><result status="valid" time="0.062736" steps="265170"/></proof>
</goal>
<goal name="and&#39;vc.39.1.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="and&#39;vc.39.1.1.0" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.088131" steps="12579"/></proof>
</goal>
<goal name="and&#39;vc.39.1.1.1" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.206378" steps="406000"/></proof>
<proof prover="4"><result status="valid" time="0.094909" steps="398138"/></proof>
</goal>
<goal name="and&#39;vc.39.1.1.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.052401" steps="80"/></proof>
Expand All @@ -716,7 +714,7 @@
<goal name="and&#39;vc.39.2" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="and&#39;vc.39.2.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.058120" steps="263688"/></proof>
<proof prover="4"><result status="valid" time="0.063540" steps="273966"/></proof>
</goal>
<goal name="and&#39;vc.39.2.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
Expand All @@ -742,7 +740,7 @@
<goal name="and&#39;vc.40" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="and&#39;vc.40.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.050306" steps="231721"/></proof>
<proof prover="4"><result status="valid" time="0.103712" steps="424427"/></proof>
</goal>
<goal name="and&#39;vc.40.1" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.119851" steps="30502"/></proof>
Expand All @@ -754,22 +752,22 @@
</theory>
<theory name="Bdd_Hashmap_Impl2" proved="true">
<goal name="hash_refn" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="747"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.003279" steps="461"/></proof>
</goal>
</theory>
<theory name="Bdd_Impl1" proved="true">
<goal name="hash_refn" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="2366"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.008572" steps="1734"/></proof>
</goal>
</theory>
<theory name="Bdd_Impl2" proved="true">
<goal name="hash_refn" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="662"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.003589" steps="439"/></proof>
</goal>
</theory>
<theory name="Bdd_Impl13" proved="true">
<goal name="assert_receiver_is_total_eq_refn" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="20"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.002133" steps="27"/></proof>
</goal>
</theory>
<theory name="Bdd_Impl19" proved="true">
Expand All @@ -779,12 +777,12 @@
</theory>
<theory name="Bdd_Impl14" proved="true">
<goal name="eq_refn" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="661"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.003799" steps="437"/></proof>
</goal>
</theory>
<theory name="Bdd_Impl7" proved="true">
<goal name="eq_refn" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="662"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.003839" steps="439"/></proof>
</goal>
</theory>
<theory name="Bdd_Impl15" proved="true">
Expand All @@ -794,7 +792,7 @@
</theory>
<theory name="Bdd_Impl0" proved="true">
<goal name="clone&#39;_refn" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="912"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.005105" steps="679"/></proof>
</goal>
</theory>
</file>
Expand Down
54 changes: 27 additions & 27 deletions creusot/tests/should_succeed/binary_search/why3session.xml
Original file line number Diff line number Diff line change
Expand Up @@ -2,95 +2,95 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="1" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="binary_search.mlcfg"/>
<theory name="BinarySearch_Impl0_LenLogic_Impl" proved="true">
<goal name="len_logic&#39;vc" expl="VC for len_logic" proved="true">
<proof prover="1"><result status="valid" time="0.010000" steps="27"/></proof>
<proof prover="0"><result status="valid" time="0.010000" steps="27"/></proof>
</goal>
</theory>
<theory name="BinarySearch_Impl0_Index" proved="true">
<goal name="index&#39;vc" expl="VC for index" proved="true">
<proof prover="1"><result status="valid" time="0.030000" steps="163"/></proof>
<proof prover="0"><result status="valid" time="0.030000" steps="162"/></proof>
</goal>
</theory>
<theory name="BinarySearch_Impl0_Len" proved="true">
<goal name="len&#39;vc" expl="VC for len" proved="true">
<proof prover="1"><result status="valid" time="0.020000" steps="164"/></proof>
<proof prover="0"><result status="valid" time="0.020000" steps="155"/></proof>
</goal>
</theory>
<theory name="BinarySearch_BinarySearch" proved="true">
<goal name="binary_search&#39;vc" expl="VC for binary_search" proved="true">
<transf name="split_vc" proved="true" >
<goal name="binary_search&#39;vc.0" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.010000" steps="10"/></proof>
<proof prover="0"><result status="valid" time="0.010000" steps="10"/></proof>
</goal>
<goal name="binary_search&#39;vc.1" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.006300" steps="13"/></proof>
<proof prover="0"><result status="valid" time="0.006300" steps="13"/></proof>
</goal>
<goal name="binary_search&#39;vc.2" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.010000" steps="24"/></proof>
<proof prover="0"><result status="valid" time="0.010000" steps="24"/></proof>
</goal>
<goal name="binary_search&#39;vc.3" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.008696" steps="29"/></proof>
<proof prover="0"><result status="valid" time="0.008696" steps="29"/></proof>
</goal>
<goal name="binary_search&#39;vc.4" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.010000" steps="34"/></proof>
<proof prover="0"><result status="valid" time="0.010000" steps="34"/></proof>
</goal>
<goal name="binary_search&#39;vc.5" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.010000" steps="65"/></proof>
<proof prover="0"><result status="valid" time="0.010000" steps="64"/></proof>
</goal>
<goal name="binary_search&#39;vc.6" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.070000" steps="48"/></proof>
<proof prover="0"><result status="valid" time="0.070000" steps="48"/></proof>
</goal>
<goal name="binary_search&#39;vc.7" expl="division by zero" proved="true">
<proof prover="1"><result status="valid" time="0.020000" steps="51"/></proof>
<proof prover="0"><result status="valid" time="0.020000" steps="51"/></proof>
</goal>
<goal name="binary_search&#39;vc.8" expl="division by zero" proved="true">
<proof prover="1"><result status="valid" time="0.050000" steps="53"/></proof>
<proof prover="0"><result status="valid" time="0.050000" steps="53"/></proof>
</goal>
<goal name="binary_search&#39;vc.9" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.030000" steps="115"/></proof>
<proof prover="0"><result status="valid" time="0.030000" steps="114"/></proof>
</goal>
<goal name="binary_search&#39;vc.10" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.040000" steps="562"/></proof>
<proof prover="0"><result status="valid" time="0.040000" steps="560"/></proof>
</goal>
<goal name="binary_search&#39;vc.11" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.030000" steps="149"/></proof>
<proof prover="0"><result status="valid" time="0.030000" steps="149"/></proof>
</goal>
<goal name="binary_search&#39;vc.12" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.025913" steps="127"/></proof>
<proof prover="0"><result status="valid" time="0.025913" steps="127"/></proof>
</goal>
<goal name="binary_search&#39;vc.13" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.020000" steps="50"/></proof>
<proof prover="0"><result status="valid" time="0.020000" steps="50"/></proof>
</goal>
<goal name="binary_search&#39;vc.14" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.015004" steps="65"/></proof>
<proof prover="0"><result status="valid" time="0.015004" steps="65"/></proof>
</goal>
<goal name="binary_search&#39;vc.15" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.060000" steps="87"/></proof>
<proof prover="0"><result status="valid" time="0.060000" steps="87"/></proof>
</goal>
<goal name="binary_search&#39;vc.16" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.120000" steps="705"/></proof>
<proof prover="0"><result status="valid" time="0.120000" steps="694"/></proof>
</goal>
<goal name="binary_search&#39;vc.17" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.030000" steps="304"/></proof>
<proof prover="0"><result status="valid" time="0.030000" steps="301"/></proof>
</goal>
<goal name="binary_search&#39;vc.18" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.120000" steps="1066"/></proof>
<proof prover="0"><result status="valid" time="0.120000" steps="1081"/></proof>
</goal>
<goal name="binary_search&#39;vc.19" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.161160" steps="2422"/></proof>
<proof prover="0"><result status="valid" time="0.161160" steps="2351"/></proof>
</goal>
<goal name="binary_search&#39;vc.20" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.090000" steps="777"/></proof>
<proof prover="0"><result status="valid" time="0.090000" steps="775"/></proof>
</goal>
<goal name="binary_search&#39;vc.21" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.331323" steps="6726"/></proof>
<proof prover="0"><result status="valid" time="0.331323" steps="7090"/></proof>
</goal>
<goal name="binary_search&#39;vc.22" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.511725" steps="10470"/></proof>
<proof prover="0"><result status="valid" time="0.511725" steps="11133"/></proof>
</goal>
</transf>
</goal>
Expand Down
4 changes: 2 additions & 2 deletions creusot/tests/should_succeed/bug/173/why3session.xml
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="1" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="173.mlcfg"/>
<theory name="C173_Test233" proved="true">
<goal name="test_233&#39;vc" expl="VC for test_233" proved="true">
<proof prover="1"><result status="valid" time="0.006587" steps="6"/></proof>
<proof prover="0"><result status="valid" time="0.006587" steps="6"/></proof>
</goal>
</theory>
</file>
Expand Down
Loading

0 comments on commit b6e36d4

Please sign in to comment.