Skip to content

Commit

Permalink
Update why3 sessions
Browse files Browse the repository at this point in the history
  • Loading branch information
@Halbaroth @jhjourdan
Halbaroth authored and jhjourdan committed Mar 10, 2025
1 parent edd9ca6 commit 87a43fb
Show file tree
Hide file tree
Showing 3 changed files with 57 additions and 28 deletions.
40 changes: 30 additions & 10 deletions tests/creusot-contracts/creusot-contracts/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,14 @@
<goal name="vc_produces_trans&#39;0.1.0.5.0" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="vc_produces_trans&#39;0.1.0.5.0.0" proved="true">
<proof prover="3" timelimit="30" memlimit="4000"><result status="valid" time="1.179406" steps="28298"/></proof>
<proof prover="3" timelimit="30" memlimit="4000"><result status="valid" time="1.405945" steps="28298"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="vc_produces_trans&#39;0.1.0.6" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.362258" steps="69879"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.673399" steps="69879"/></proof>
</goal>
</transf>
</goal>
Expand Down Expand Up @@ -140,12 +140,12 @@
<goal name="vc_produces_trans&#39;0.1.0.5" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_produces_trans&#39;0.1.0.5.0" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.151694" steps="32930"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.936249" steps="32930"/></proof>
</goal>
</transf>
</goal>
<goal name="vc_produces_trans&#39;0.1.0.6" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.356152" steps="61479"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.507270" steps="61479"/></proof>
</goal>
</transf>
</goal>
Expand Down Expand Up @@ -197,7 +197,7 @@
<goal name="vc_produces_trans&#39;0.1.0.5" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_produces_trans&#39;0.1.0.5.0" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.179987" steps="33103"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.701776" steps="33103"/></proof>
</goal>
</transf>
</goal>
Expand Down Expand Up @@ -338,6 +338,26 @@
<proof prover="3"><result status="valid" time="0.037413" steps="0"/></proof>
</goal>
</theory>
<theory name="M_creusot_contracts__stdqy35z1__collections__hash_set__qyi3953735896298504416__produces_refl__refines" proved="true">
<goal name="refines" proved="true">
<proof prover="3"><result status="valid" time="0.020394" steps="0"/></proof>
</goal>
</theory>
<theory name="M_creusot_contracts__stdqy35z1__collections__hash_set__qyi3953735896298504416__produces_refl" proved="true">
<goal name="vc_produces_refl&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.022371" steps="58"/></proof>
</goal>
</theory>
<theory name="M_creusot_contracts__stdqy35z1__collections__hash_set__qyi3953735896298504416__produces_trans__refines" proved="true">
<goal name="refines" proved="true">
<proof prover="2"><result status="valid" time="0.035844" steps="5259"/></proof>
</goal>
</theory>
<theory name="M_creusot_contracts__stdqy35z1__collections__hash_set__qyi3953735896298504416__produces_trans" proved="true">
<goal name="vc_produces_trans&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.018660" steps="0"/></proof>
</goal>
</theory>
<theory name="M_creusot_contracts__logic__fset__qyi15838233236912513155__ext_eq" proved="true">
<goal name="vc_ext_eq&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.026481" steps="7"/></proof>
Expand Down Expand Up @@ -404,7 +424,7 @@
</theory>
<theory name="M_creusot_contracts__logic__fset__unions_union" proved="true">
<goal name="vc_unions_union&#39;0" proved="true">
<proof prover="0"><result status="valid" time="1.102882" steps="2240462"/></proof>
<proof prover="0"><result status="valid" time="1.669795" steps="2240462"/></proof>
</goal>
</theory>
<theory name="M_creusot_contracts__logic__fset__map_union" proved="true">
Expand Down Expand Up @@ -453,7 +473,7 @@
<proof prover="3"><result status="valid" time="0.137858" steps="1674"/></proof>
</goal>
<goal name="vc_concat_empty&#39;0.3" proved="true">
<proof prover="2"><result status="valid" time="0.641501" steps="106183"/></proof>
<proof prover="2"><result status="valid" time="0.844308" steps="106183"/></proof>
</goal>
</transf>
</goal>
Expand Down Expand Up @@ -2881,7 +2901,7 @@
</theory>
<theory name="M_creusot_contracts__stdqy35z1__iter__map_inv__qyi8002351551305542163__next" proved="true">
<goal name="vc_next&#39;0" proved="true">
<proof prover="2"><result status="valid" time="0.135717" steps="28920"/></proof>
<proof prover="2"><result status="valid" time="0.273236" steps="28920"/></proof>
</goal>
</theory>
<theory name="M_creusot_contracts__stdqy35z1__iter__map_inv__qyi6396809843712938673__preservation_inv" proved="true">
Expand All @@ -2899,7 +2919,7 @@
<goal name="vc_produces_one&#39;0.0" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_produces_one&#39;0.0.0" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.611275" steps="142336"/></proof>
<proof prover="1" timelimit="1"><result status="valid" time="1.001072" steps="142336"/></proof>
</goal>
<goal name="vc_produces_one&#39;0.0.1" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.144536" steps="243138"/></proof>
Expand Down Expand Up @@ -3129,7 +3149,7 @@
</theory>
<theory name="M_creusot_contracts__stdqy35z1__iter__zip__qyi9055347977946847871__produces_trans" proved="true">
<goal name="vc_produces_trans&#39;0" proved="true">
<proof prover="3"><result status="valid" time="1.349723" steps="20949"/></proof>
<proof prover="3"><result status="valid" time="1.678320" steps="20949"/></proof>
</goal>
</theory>
<theory name="M_creusot_contracts__stdqy35z1__option__extern_spec_std_option_T_Option_T_unwrap_or_else_body" proved="true">
Expand Down
Binary file modified tests/creusot-contracts/creusot-contracts/why3shapes.gz
View file
Binary file not shown.
45 changes: 27 additions & 18 deletions tests/should_succeed/cc/collections/proof.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,39 +6,48 @@
{ "prover": "[email protected]", "size": 45, "time": 0.426 }
],
"proofs": {
"M_collections__hashset_difference": {
"vc_collect'0": { "prover": "[email protected]", "time": 0.009 },
"vc_copied'0": { "prover": "[email protected]", "time": 0.014 },
"vc_difference'0": { "prover": "[email protected]", "time": 0.011 },
"vc_hashset_difference'0": {
"prover": "[email protected]",
"time": 0.051
}
},
"M_collections__hashset_intersection": {
"vc_collect'0": { "prover": "[email protected]", "time": 0.022 },
"vc_copied'0": { "prover": "[email protected]", "time": 0.045 },
"vc_collect'0": { "prover": "[email protected]", "time": 0.009 },
"vc_copied'0": { "prover": "[email protected]", "time": 0.014 },
"vc_hashset_intersection'0": {
"prover": "[email protected]",
"time": 0.098
"time": 0.045
},
"vc_intersection'0": { "prover": "[email protected]", "time": 0.018 }
},
"M_collections__roundtrip_hashmap_into_iter": {
"vc_collect'0": { "prover": "[email protected]", "time": 0.024 },
"vc_into_iter'0": { "prover": "[email protected]", "time": 0.02 },
"vc_collect'0": { "prover": "[email protected]", "time": 0.008 },
"vc_into_iter'0": { "prover": "[email protected]", "time": 0.009 },
"vc_roundtrip_hashmap_into_iter'0": {
"tactic": "split_vc",
"children": [
{ "prover": "[email protected]", "time": 0.025 },
{ "prover": "[email protected]", "time": 0.037 },
{ "prover": "[email protected]", "time": 0.025 },
{ "prover": "[email protected]", "time": 0.04 },
{ "prover": "[email protected]", "time": 0.013 },
{ "prover": "[email protected]", "time": 0.01 },
{ "prover": "[email protected]", "time": 0.02 },
{ "prover": "[email protected]", "time": 0.041 },
{ "prover": "[email protected]", "time": 0.028 },
{ "prover": "[email protected]", "time": 0.257 }
{ "prover": "[email protected]", "time": 0.034 }
]
}
},
"M_collections__roundtrip_hashmap_iter": {
"vc_collect'0": { "prover": "[email protected]", "time": 0.031 },
"vc_collect'0": { "prover": "[email protected]", "time": 0.006 },
"vc_iter'0": { "prover": "[email protected]", "time": 0.018 },
"vc_roundtrip_hashmap_iter'0": {
"tactic": "split_vc",
"children": [
{ "prover": "[email protected]", "time": 0.023 },
{ "prover": "[email protected]", "time": 0.045 },
{ "prover": "[email protected]", "time": 0.009 },
{ "prover": "[email protected]", "time": 0.009 },
{ "prover": "[email protected]", "time": 0.035 },
{ "prover": "[email protected]", "time": 0.019 }
]
Expand All @@ -50,26 +59,26 @@
"vc_roundtrip_hashmap_iter_mut'0": {
"tactic": "split_vc",
"children": [
{ "prover": "[email protected]", "time": 0.029 },
{ "prover": "[email protected]", "time": 0.033 },
{ "prover": "[email protected]", "time": 0.01 },
{ "prover": "[email protected]", "time": 0.011 },
{ "prover": "[email protected]", "time": 0.036 },
{ "prover": "[email protected]", "time": 0.103 },
{ "prover": "[email protected]", "time": 0.034 },
{ "prover": "[email protected]", "time": 0.017 },
{ "prover": "[email protected]", "time": 0.033 }
]
}
},
"M_collections__roundtrip_hashset_into_iter": {
"vc_collect'0": { "prover": "[email protected]", "time": 0.029 },
"vc_collect'0": { "prover": "[email protected]", "time": 0.008 },
"vc_into_iter'0": { "prover": "[email protected]", "time": 0.016 },
"vc_roundtrip_hashset_into_iter'0": {
"prover": "[email protected]",
"time": 0.05
}
},
"M_collections__roundtrip_hashset_iter": {
"vc_collect'0": { "prover": "[email protected]", "time": 0.021 },
"vc_iter'0": { "prover": "[email protected]", "time": 0.031 },
"vc_collect'0": { "prover": "[email protected]", "time": 0.009 },
"vc_iter'0": { "prover": "[email protected]", "time": 0.007 },
"vc_roundtrip_hashset_iter'0": { "prover": "[email protected]", "time": 0.041 }
}
}
Expand Down

0 comments on commit 87a43fb

Please sign in to comment.