Skip to content

Commit 671fc14

Browse files
joffreyhuguetjoffreyhuguet
committed
Merge branch 'topic/kanig-sessions' into 'master'
Another attempt to recreate sessions no-issue-check See merge request eng/spark/spark2014!2244
2 parents bf57c9f + 93c9b59 commit 671fc14

File tree

271 files changed

+4177
-4177
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

271 files changed

+4177
-4177
lines changed

‎testsuite/gnatprove/tests/1041__hashed_sets/proof/sessions/0200c1ffd3a997443258-rivate_model__lemma_reachable_ext/why3session.xml‎

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@
2727
<proof prover="3"><result status="valid" steps="1"/></proof>
2828
</goal>
2929
<goal name="def&#39;vc.4" proved="true">
30-
<proof prover="0"><result status="highfailure"/></proof>
30+
<proof prover="0"><result status="valid" steps="16"/></proof>
3131
<proof prover="1"><result status="valid" steps="2534"/></proof>
3232
<proof prover="2"><result status="valid" steps="1678"/></proof>
3333
</goal>
@@ -42,23 +42,23 @@
4242
<proof prover="2"><result status="valid" steps="1693"/></proof>
4343
</goal>
4444
<goal name="def&#39;vc.7" proved="true">
45-
<proof prover="0"><result status="highfailure"/></proof>
45+
<proof prover="0"><result status="valid" steps="2"/></proof>
4646
<proof prover="1"><result status="valid" steps="2716"/></proof>
4747
<proof prover="2"><result status="valid" steps="1763"/></proof>
4848
</goal>
4949
<goal name="def&#39;vc.8" proved="true">
50-
<proof prover="0"><result status="highfailure"/></proof>
50+
<proof prover="0"><result status="valid" steps="2"/></proof>
5151
<proof prover="1"><result status="valid" steps="2716"/></proof>
5252
<proof prover="2"><result status="valid" steps="1761"/></proof>
5353
</goal>
5454
<goal name="def&#39;vc.9" proved="true">
55-
<proof prover="0"><result status="highfailure"/></proof>
56-
<proof prover="1"><result status="highfailure"/></proof>
55+
<proof prover="0"><result status="valid" steps="56"/></proof>
56+
<proof prover="1"><result status="valid" steps="4891"/></proof>
5757
<proof prover="2"><result status="valid" steps="15622"/></proof>
5858
</goal>
5959
<goal name="def&#39;vc.10" proved="true">
6060
<proof prover="0"><result status="highfailure"/></proof>
61-
<proof prover="1"><result status="highfailure"/></proof>
61+
<proof prover="1"><result status="valid" steps="4857"/></proof>
6262
<proof prover="2"><result status="valid" steps="15623"/></proof>
6363
</goal>
6464
<goal name="def&#39;vc.11" proved="true">
@@ -67,8 +67,8 @@
6767
<proof prover="2"><result status="valid" steps="16561"/></proof>
6868
</goal>
6969
<goal name="def&#39;vc.12" proved="true">
70-
<proof prover="0"><result status="highfailure"/></proof>
71-
<proof prover="1"><result status="highfailure"/></proof>
70+
<proof prover="0"><result status="valid" steps="76"/></proof>
71+
<proof prover="1"><result status="valid" steps="6596"/></proof>
7272
<proof prover="2"><result status="valid" steps="16505"/></proof>
7373
</goal>
7474
<goal name="def&#39;vc.13" proved="true">
@@ -77,13 +77,13 @@
7777
<proof prover="2"><result status="valid" steps="7871"/></proof>
7878
</goal>
7979
<goal name="def&#39;vc.14" proved="true">
80-
<proof prover="0"><result status="highfailure"/></proof>
81-
<proof prover="1"><result status="valid"/></proof>
80+
<proof prover="0"><result status="valid" steps="92"/></proof>
81+
<proof prover="1"><result status="valid" steps="5585"/></proof>
8282
<proof prover="2"><result status="valid" steps="16520"/></proof>
8383
</goal>
8484
<goal name="def&#39;vc.15" proved="true">
85-
<proof prover="0"><result status="highfailure"/></proof>
86-
<proof prover="1"><result status="highfailure"/></proof>
85+
<proof prover="0"><result status="valid" steps="93"/></proof>
86+
<proof prover="1"><result status="valid" steps="6406"/></proof>
8787
<proof prover="2"><result status="valid" steps="17755"/></proof>
8888
</goal>
8989
<goal name="def&#39;vc.16" proved="true">
@@ -97,8 +97,8 @@
9797
<proof prover="2"><result status="valid" steps="3227"/></proof>
9898
</goal>
9999
<goal name="def&#39;vc.18" proved="true">
100-
<proof prover="0"><result status="highfailure"/></proof>
101-
<proof prover="1"><result status="highfailure"/></proof>
100+
<proof prover="0"><result status="valid" steps="8"/></proof>
101+
<proof prover="1"><result status="valid" steps="4029"/></proof>
102102
<proof prover="2"><result status="valid" steps="3429"/></proof>
103103
</goal>
104104
<goal name="def&#39;vc.19" proved="true">

‎testsuite/gnatprove/tests/1041__hashed_sets/proof/sessions/043a665ff3b240189a26-ns__private_model__ll_has_element/why3session.xml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@
3333
<proof prover="2"><result status="valid" steps="11353"/></proof>
3434
</goal>
3535
<goal name="def&#39;vc.4" proved="true">
36-
<proof prover="0"><result status="highfailure"/></proof>
36+
<proof prover="0"><result status="valid" steps="173"/></proof>
3737
<proof prover="1"><result status="highfailure"/></proof>
3838
<proof prover="2"><result status="valid" steps="11823"/></proof>
3939
</goal>

0 commit comments

Comments
 (0)