Skip to content

Commit

Permalink
Update test proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
@arnaudgolfouse
arnaudgolfouse committed Dec 11, 2023
1 parent f9ab714 commit 90034f1
Show file tree
Hide file tree
Showing 170 changed files with 2,980 additions and 2,920 deletions.
2 changes: 1 addition & 1 deletion creusot/tests/should_succeed/100doors/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
<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.138920" steps="699145"/></proof>
<proof prover="1"><result status="valid" time="0.138920" steps="685552"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified creusot/tests/should_succeed/100doors/why3shapes.gz
View file
Binary file not shown.
2 changes: 1 addition & 1 deletion creusot/tests/should_succeed/all_zero/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
<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="0"><result status="valid" time="0.038573" steps="874"/></proof>
<proof prover="0"><result status="valid" time="0.038573" steps="893"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified creusot/tests/should_succeed/all_zero/why3shapes.gz
View file
Binary file not shown.
355 changes: 177 additions & 178 deletions creusot/tests/should_succeed/bdd/why3session.xml
View file

Large diffs are not rendered by default.

Binary file modified creusot/tests/should_succeed/bdd/why3shapes.gz
View file
Binary file not shown.
20 changes: 10 additions & 10 deletions creusot/tests/should_succeed/binary_search/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,12 @@
</theory>
<theory name="BinarySearch_Impl0_Index" proved="true">
<goal name="index&#39;vc" expl="VC for index" proved="true">
<proof prover="0"><result status="valid" time="0.030000" steps="164"/></proof>
<proof prover="0"><result status="valid" time="0.030000" steps="163"/></proof>
</goal>
</theory>
<theory name="BinarySearch_Impl0_Len" proved="true">
<goal name="len&#39;vc" expl="VC for len" proved="true">
<proof prover="0"><result status="valid" time="0.020000" steps="156"/></proof>
<proof prover="0"><result status="valid" time="0.020000" steps="155"/></proof>
</goal>
</theory>
<theory name="BinarySearch_BinarySearch" proved="true">
Expand All @@ -42,7 +42,7 @@
<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="0"><result status="valid" time="0.070000" steps="49"/></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="0"><result status="valid" time="0.020000" steps="51"/></proof>
Expand All @@ -51,7 +51,7 @@
<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="0"><result status="valid" time="0.030000" steps="116"/></proof>
<proof prover="0"><result status="valid" time="0.030000" steps="115"/></proof>
</goal>
<goal name="binary_search&#39;vc.10" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.040000" steps="567"/></proof>
Expand All @@ -72,25 +72,25 @@
<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="0"><result status="valid" time="0.120000" steps="706"/></proof>
<proof prover="0"><result status="valid" time="0.120000" steps="704"/></proof>
</goal>
<goal name="binary_search&#39;vc.17" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.030000" steps="299"/></proof>
<proof prover="0"><result status="valid" time="0.030000" steps="303"/></proof>
</goal>
<goal name="binary_search&#39;vc.18" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.120000" steps="1068"/></proof>
</goal>
<goal name="binary_search&#39;vc.19" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.304838" steps="2428"/></proof>
<proof prover="0"><result status="valid" time="0.152441" steps="2437"/></proof>
</goal>
<goal name="binary_search&#39;vc.20" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.090000" steps="781"/></proof>
<proof prover="0"><result status="valid" time="0.090000" steps="780"/></proof>
</goal>
<goal name="binary_search&#39;vc.21" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.632579" steps="7061"/></proof>
<proof prover="0"><result status="valid" time="0.326597" steps="7066"/></proof>
</goal>
<goal name="binary_search&#39;vc.22" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.976706" steps="11672"/></proof>
<proof prover="0"><result status="valid" time="0.529507" steps="11710"/></proof>
</goal>
</transf>
</goal>
Expand Down
Binary file modified creusot/tests/should_succeed/binary_search/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/bug/206/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/bug/463/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/bug/552/why3shapes.gz
View file
Binary file not shown.
2 changes: 1 addition & 1 deletion creusot/tests/should_succeed/bug/682/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
</theory>
<theory name="C682_Foo" proved="true">
<goal name="foo&#39;vc" expl="VC for foo" proved="true">
<proof prover="0"><result status="valid" time="0.018181" steps="440"/></proof>
<proof prover="0"><result status="valid" time="0.018181" steps="405"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified creusot/tests/should_succeed/bug/682/why3shapes.gz
View file
Binary file not shown.
14 changes: 12 additions & 2 deletions creusot/tests/should_succeed/bug/874/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="2" name="Z3" version="4.8.12" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="0" name="Z3" version="4.12.2" timelimit="1" steplimit="0" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="874.mlcfg"/>
<theory name="C874_CanExtend" proved="true">
Expand All @@ -28,7 +30,15 @@
<proof prover="3"><result status="valid" time="0.010587" steps="63"/></proof>
</goal>
<goal name="can_extend&#39;vc.6" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.060098" steps="197056"/></proof>
<proof prover="0" memlimit="1000"><result status="timeout" time="1.000000" steps="3591024"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="253865"/></proof>
<proof prover="3"><result status="timeout" time="1.000000" steps="17714"/></proof>
<proof prover="4"><result status="timeout" time="1.000000" steps="223747"/></proof>
<transf name="split_vc" proved="true" >
<goal name="can_extend&#39;vc.6.0" expl="assertion" proved="true">
<proof prover="0" timelimit="10"><result status="valid" time="9.474103" steps="20751146"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
Expand Down
Binary file modified creusot/tests/should_succeed/bug/874/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/bug/eq_panic/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/bug/two_phase/why3shapes.gz
View file
Binary file not shown.
2 changes: 1 addition & 1 deletion creusot/tests/should_succeed/cell/01/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
<path name=".."/><path name="01.mlcfg"/>
<theory name="C01_AddsTwo" proved="true">
<goal name="adds_two&#39;vc" expl="VC for adds_two" proved="true">
<proof prover="0"><result status="valid" time="0.033868" steps="676"/></proof>
<proof prover="0"><result status="valid" time="0.033868" steps="679"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified creusot/tests/should_succeed/cell/01/why3shapes.gz
View file
Binary file not shown.
24 changes: 12 additions & 12 deletions creusot/tests/should_succeed/cell/02/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,19 +2,19 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Z3" version="4.12.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.8.12" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="02.mlcfg"/>
<theory name="C02_Fib_Impl" proved="true">
<goal name="fib&#39;vc" expl="VC for fib" proved="true">
<proof prover="4"><result status="valid" time="0.008370" steps="487"/></proof>
<proof prover="0"><result status="valid" time="0.008370" steps="428"/></proof>
</goal>
</theory>
<theory name="C02_LemmaFibBound_Impl" proved="true">
<goal name="lemma_fib_bound&#39;vc" expl="VC for lemma_fib_bound" proved="true">
<proof prover="4"><result status="valid" time="0.012781" steps="10102"/></proof>
<proof prover="0"><result status="valid" time="0.012781" steps="9016"/></proof>
</goal>
</theory>
<theory name="C02_FibMemo" proved="true">
Expand All @@ -24,11 +24,11 @@
<proof prover="5"><result status="valid" time="0.008535" steps="10"/></proof>
</goal>
<goal name="fib_memo&#39;vc.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.064765" steps="84037"/></proof>
<proof prover="0"><result status="valid" time="0.064765" steps="71155"/></proof>
<proof prover="5"><result status="valid" time="0.015501" steps="22"/></proof>
</goal>
<goal name="fib_memo&#39;vc.2" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.021326" steps="84108"/></proof>
<proof prover="0"><result status="valid" time="0.021326" steps="71218"/></proof>
<proof prover="5"><result status="valid" time="0.012298" steps="23"/></proof>
</goal>
<goal name="fib_memo&#39;vc.3" expl="precondition" proved="true">
Expand Down Expand Up @@ -59,7 +59,7 @@
<proof prover="5"><result status="valid" time="0.009606" steps="39"/></proof>
</goal>
<goal name="fib_memo&#39;vc.12" expl="integer overflow" proved="true">
<proof prover="5"><result status="valid" time="0.103941" steps="1028"/></proof>
<proof prover="5"><result status="valid" time="0.103941" steps="1030"/></proof>
</goal>
<goal name="fib_memo&#39;vc.13" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
Expand All @@ -68,7 +68,7 @@
<goal name="fib_memo&#39;vc.13.0.0" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="fib_memo&#39;vc.13.0.0.0" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.024054" steps="108072"/></proof>
<proof prover="0"><result status="valid" time="0.024054" steps="92696"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -79,7 +79,7 @@
<goal name="fib_memo&#39;vc.13.1.0" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="fib_memo&#39;vc.13.1.0.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.212541" steps="1844"/></proof>
<proof prover="5"><result status="valid" time="0.212541" steps="1840"/></proof>
</goal>
<goal name="fib_memo&#39;vc.13.1.0.1" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.043215" steps="249"/></proof>
Expand All @@ -91,14 +91,14 @@
</transf>
</goal>
<goal name="fib_memo&#39;vc.14" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.011911" steps="7686"/></proof>
<proof prover="0"><result status="valid" time="0.011911" steps="8814"/></proof>
<proof prover="5"><result status="valid" time="0.028068" steps="18"/></proof>
</goal>
<goal name="fib_memo&#39;vc.15" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.009702" steps="55"/></proof>
</goal>
<goal name="fib_memo&#39;vc.16" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.068972" steps="14325"/></proof>
<proof prover="1"><result status="valid" time="0.068972" steps="13689"/></proof>
<proof prover="5"><result status="valid" time="0.029729" steps="56"/></proof>
</goal>
<goal name="fib_memo&#39;vc.17" expl="precondition" proved="true">
Expand All @@ -108,11 +108,11 @@
<proof prover="5"><result status="valid" time="0.117430" steps="23"/></proof>
</goal>
<goal name="fib_memo&#39;vc.19" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.023987" steps="106854"/></proof>
<proof prover="0"><result status="valid" time="0.023987" steps="89729"/></proof>
<proof prover="5"><result status="valid" time="0.022739" steps="59"/></proof>
</goal>
<goal name="fib_memo&#39;vc.20" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.107580" steps="16945"/></proof>
<proof prover="1"><result status="valid" time="0.107580" steps="16279"/></proof>
</goal>
</transf>
</goal>
Expand Down
Binary file modified creusot/tests/should_succeed/cell/02/why3shapes.gz
View file
Binary file not shown.
Loading

0 comments on commit 90034f1

Please sign in to comment.