Skip to content

Commit

Permalink
update sessions
Browse files Browse the repository at this point in the history
  • Loading branch information
@xldenis
xldenis committed May 23, 2024
1 parent b36e6ef commit c212b23
Show file tree
Hide file tree
Showing 32 changed files with 3,470 additions and 3,138 deletions.
21 changes: 0 additions & 21 deletions creusot/tests/should_succeed/index_range/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,27 +191,6 @@
<goal name="vc_test_range_to.56" proved="true">
<proof prover="2"><result status="valid" time="0.016002" steps="772"/></proof>
</goal>
<goal name="test_range_to&#39;vc.63" expl="unreachable point">
<proof prover="2"><result status="valid" time="0.012461" steps="43"/></proof>
</goal>
<goal name="test_range_to&#39;vc.61" expl="unreachable point">
<proof prover="2"><result status="valid" time="0.024082" steps="238"/></proof>
</goal>
<goal name="test_range_to&#39;vc.56" expl="unreachable point">
<proof prover="2"><result status="valid" time="0.027625" steps="229"/></proof>
</goal>
<goal name="test_range_to&#39;vc.51" expl="unreachable point">
<proof prover="0"><result status="valid" time="0.012386" steps="4103"/></proof>
</goal>
<goal name="test_range_to&#39;vc.46" expl="unreachable point">
<proof prover="0"><result status="valid" time="0.012573" steps="4076"/></proof>
</goal>
<goal name="test_range_to&#39;vc.41" expl="unreachable point">
<proof prover="2"><result status="valid" time="0.019084" steps="208"/></proof>
</goal>
<goal name="test_range_to&#39;vc.12" expl="assertion">
<proof prover="2"><result status="valid" time="0.032146" steps="392"/></proof>
</goal>
</transf>
</goal>
</theory>
Expand Down
Binary file modified creusot/tests/should_succeed/index_range/why3shapes.gz
View file
Binary file not shown.
7 changes: 1 addition & 6 deletions creusot/tests/should_succeed/ite_normalize/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,18 +5,13 @@
<prover id="0" name="Alt-Ergo" version="2.5.3" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.12.4" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="coma">
<file format="coma" proved="true">
<path name=".."/><path name="ite_normalize.coma"/>
<theory name="IteNormalize_Impl6_Clone" proved="true">
<goal name="vc_clone&#39;" proved="true">
<proof prover="0"><result status="valid" time="0.015003" steps="81"/></proof>
</goal>
</theory>
<theory name="IteNormalize_Impl5_Ite">
<goal name="ite&#39;vc" expl="VC for ite">
<proof prover="0"><result status="valid" time="0.003573" steps="7"/></proof>
</goal>
</theory>
<theory name="IteNormalize_Impl5_Transpose" proved="true">
<goal name="vc_transpose" proved="true">
<proof prover="4"><result status="valid" time="0.013467" steps="3667"/></proof>
Expand Down
Binary file modified creusot/tests/should_succeed/ite_normalize/why3shapes.gz
View file
Binary file not shown.
7 changes: 1 addition & 6 deletions creusot/tests/should_succeed/iterators/01_range/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
"https://www.why3.org/why3session.dtd">
<why3session shape_version="6">
<prover id="1" name="Alt-Ergo" version="2.5.3" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="coma">
<file format="coma" proved="true">
<path name=".."/><path name="01_range.coma"/>
<theory name="C01Range_Impl0_ProducesRefl_Impl" proved="true">
<goal name="vc_produces_refl" proved="true">
Expand All @@ -20,11 +20,6 @@
<proof prover="1"><result status="valid" time="0.025654" steps="762"/></proof>
</goal>
</theory>
<theory name="C01Range_Impl1_IntoIter">
<goal name="into_iter&#39;vc" expl="VC for into_iter">
<proof prover="1"><result status="valid" time="0.008723" steps="1"/></proof>
</goal>
</theory>
<theory name="C01Range_SumRange" proved="true">
<goal name="vc_sum_range" proved="true">
<proof prover="1"><result status="valid" time="0.130911" steps="2771"/></proof>
Expand Down
Binary file modified creusot/tests/should_succeed/iterators/01_range/why3shapes.gz
View file
Binary file not shown.
190 changes: 92 additions & 98 deletions creusot/tests/should_succeed/iterators/08_collect_extend/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,160 +6,154 @@
<file format="coma" proved="true">
<path name=".."/><path name="08_collect_extend.coma"/>
<theory name="C08CollectExtend_Extend" proved="true">
<goal name="extend&#39;vc" expl="VC for extend" proved="true">
<goal name="vc_extend" proved="true">
<transf name="split_vc" proved="true" >
<goal name="extend&#39;vc.0" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.010431" steps="10"/></proof>
<goal name="vc_extend.0" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.013467" steps="6"/></proof>
</goal>
<goal name="extend&#39;vc.1" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.017170" steps="12"/></proof>
<goal name="vc_extend.1" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.009607" steps="8"/></proof>
</goal>
<goal name="extend&#39;vc.2" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.009746" steps="12"/></proof>
<goal name="vc_extend.2" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.017170" steps="8"/></proof>
</goal>
<goal name="extend&#39;vc.3" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.018129" steps="19"/></proof>
<goal name="vc_extend.3" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.020258" steps="14"/></proof>
</goal>
<goal name="extend&#39;vc.4" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.015389" steps="25"/></proof>
<goal name="vc_extend.4" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.019771" steps="18"/></proof>
</goal>
<goal name="extend&#39;vc.5" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.013215" steps="27"/></proof>
<goal name="vc_extend.5" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.010536" steps="80"/></proof>
</goal>
<goal name="extend&#39;vc.6" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.011051" steps="29"/></proof>
<goal name="vc_extend.6" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.060952" steps="24"/></proof>
</goal>
<goal name="extend&#39;vc.7" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.014037" steps="31"/></proof>
<goal name="vc_extend.7" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.014255" steps="26"/></proof>
</goal>
<goal name="extend&#39;vc.8" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.014255" steps="105"/></proof>
<goal name="vc_extend.8" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.013215" steps="26"/></proof>
</goal>
<goal name="extend&#39;vc.9" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.016408" steps="53"/></proof>
<goal name="vc_extend.9" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.016940" steps="34"/></proof>
</goal>
<goal name="extend&#39;vc.10" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.019771" steps="56"/></proof>
<goal name="vc_extend.10" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.019508" steps="37"/></proof>
</goal>
<goal name="extend&#39;vc.11" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.010855" steps="61"/></proof>
<goal name="vc_extend.11" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.018129" steps="42"/></proof>
</goal>
<goal name="extend&#39;vc.12" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.010879" steps="63"/></proof>
<goal name="vc_extend.12" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.010879" steps="44"/></proof>
</goal>
<goal name="extend&#39;vc.13" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.013467" steps="68"/></proof>
<goal name="vc_extend.13" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.010431" steps="48"/></proof>
</goal>
<goal name="extend&#39;vc.14" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.021012" steps="221"/></proof>
<goal name="vc_extend.14" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.021012" steps="157"/></proof>
</goal>
<goal name="extend&#39;vc.15" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.020258" steps="68"/></proof>
<goal name="vc_extend.15" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.015389" steps="47"/></proof>
</goal>
<goal name="extend&#39;vc.16" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.019508" steps="82"/></proof>
<goal name="vc_extend.16" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.010855" steps="51"/></proof>
</goal>
<goal name="extend&#39;vc.17" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.016940" steps="94"/></proof>
<goal name="vc_extend.17" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.009746" steps="57"/></proof>
</goal>
<goal name="extend&#39;vc.18" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.009607" steps="96"/></proof>
<goal name="vc_extend.18" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.016408" steps="59"/></proof>
</goal>
<goal name="extend&#39;vc.19" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.010536" steps="93"/></proof>
<goal name="vc_extend.19" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.026590" steps="756"/></proof>
</goal>
<goal name="extend&#39;vc.20" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.026590" steps="426"/></proof>
<goal name="vc_extend.20" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.013662" steps="61"/></proof>
</goal>
<goal name="extend&#39;vc.21" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.013662" steps="99"/></proof>
<goal name="vc_extend.21" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.014037" steps="508"/></proof>
</goal>
<goal name="extend&#39;vc.22" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.060952" steps="814"/></proof>
</goal>
<goal name="extend&#39;vc.23" expl="unreachable point" proved="true">
<proof prover="1"><result status="valid" time="0.015385" steps="65"/></proof>
<goal name="vc_extend.22" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.011051" steps="62"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="C08CollectExtend_Collect" proved="true">
<goal name="collect&#39;vc" expl="VC for collect" proved="true">
<goal name="vc_collect" proved="true">
<transf name="split_vc" proved="true" >
<goal name="collect&#39;vc.0" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.015097" steps="8"/></proof>
</goal>
<goal name="collect&#39;vc.1" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.015011" steps="8"/></proof>
<goal name="vc_collect.0" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.013302" steps="6"/></proof>
</goal>
<goal name="collect&#39;vc.2" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.007620" steps="15"/></proof>
<goal name="vc_collect.1" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.015097" steps="6"/></proof>
</goal>
<goal name="collect&#39;vc.3" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.014669" steps="21"/></proof>
<goal name="vc_collect.2" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.009751" steps="12"/></proof>
</goal>
<goal name="collect&#39;vc.4" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.011721" steps="23"/></proof>
<goal name="vc_collect.3" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.012764" steps="16"/></proof>
</goal>
<goal name="collect&#39;vc.5" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.012023" steps="25"/></proof>
<goal name="vc_collect.4" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.011855" steps="38"/></proof>
</goal>
<goal name="collect&#39;vc.6" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.003769" steps="49"/></proof>
<goal name="vc_collect.5" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.003769" steps="22"/></proof>
</goal>
<goal name="collect&#39;vc.7" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.013070" steps="43"/></proof>
<goal name="vc_collect.6" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.012023" steps="22"/></proof>
</goal>
<goal name="collect&#39;vc.8" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.012764" steps="46"/></proof>
<goal name="vc_collect.7" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.018927" steps="30"/></proof>
</goal>
<goal name="collect&#39;vc.9" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.007832" steps="51"/></proof>
<goal name="vc_collect.8" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.017839" steps="33"/></proof>
</goal>
<goal name="collect&#39;vc.10" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.010948" steps="53"/></proof>
<goal name="vc_collect.9" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.007620" steps="38"/></proof>
</goal>
<goal name="collect&#39;vc.11" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.014014" steps="142"/></proof>
<goal name="vc_collect.10" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.010948" steps="40"/></proof>
</goal>
<goal name="collect&#39;vc.12" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.013452" steps="68"/></proof>
<goal name="vc_collect.11" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.013452" steps="44"/></proof>
</goal>
<goal name="collect&#39;vc.13" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.009751" steps="58"/></proof>
<goal name="vc_collect.12" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.014014" steps="103"/></proof>
</goal>
<goal name="collect&#39;vc.14" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.017839" steps="72"/></proof>
<goal name="vc_collect.13" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.014669" steps="43"/></proof>
</goal>
<goal name="collect&#39;vc.15" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.018927" steps="82"/></proof>
<goal name="vc_collect.14" expl="type invariant" proved="true">
<proof prover="1"><result status="valid" time="0.007832" steps="47"/></proof>
</goal>
<goal name="collect&#39;vc.16" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.013302" steps="84"/></proof>
<goal name="vc_collect.15" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.015011" steps="53"/></proof>
</goal>
<goal name="collect&#39;vc.17" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.011855" steps="81"/></proof>
<goal name="vc_collect.16" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.013070" steps="55"/></proof>
</goal>
<goal name="collect&#39;vc.18" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.023596" steps="349"/></proof>
<goal name="vc_collect.17" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.023596" steps="337"/></proof>
</goal>
<goal name="collect&#39;vc.19" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.024815" steps="416"/></proof>
<goal name="vc_collect.18" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.011721" steps="343"/></proof>
</goal>
<goal name="collect&#39;vc.20" expl="unreachable point" proved="true">
<proof prover="1"><result status="valid" time="0.009954" steps="55"/></proof>
<goal name="vc_collect.19" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.024815" steps="56"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="C08CollectExtend_ExtendIndex" proved="true">
<goal name="extend_index&#39;vc" expl="VC for extend_index" proved="true">
<proof prover="1"><result status="valid" time="0.037507" steps="492"/></proof>
<goal name="vc_extend_index" proved="true">
<proof prover="1"><result status="valid" time="0.037507" steps="638"/></proof>
</goal>
</theory>
<theory name="C08CollectExtend_CollectExample" proved="true">
<goal name="collect_example&#39;vc" expl="VC for collect_example" proved="true">
<proof prover="1"><result status="valid" time="0.009049" steps="66"/></proof>
<goal name="vc_collect_example" proved="true">
<proof prover="1"><result status="valid" time="0.009049" steps="52"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz
View file
Binary file not shown.
Loading

0 comments on commit c212b23

Please sign in to comment.