Skip to content

Commit 18fbe95

Browse files
xldenisxldenis
committed
Update tests
1 parent e869149 commit 18fbe95

File tree

90 files changed

+1064
-1212
lines changed

Some content is hidden

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

90 files changed

+1064
-1212
lines changed

‎creusot/tests/should_succeed/bdd/why3session.xml‎

Lines changed: 96 additions & 96 deletions
Large diffs are not rendered by default.

‎creusot/tests/should_succeed/bdd/why3shapes.gz‎

-179 Bytes
Binary file not shown.

‎creusot/tests/should_succeed/binary_search/why3session.xml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -72,13 +72,13 @@
7272
<proof prover="1"><result status="valid" time="0.18" steps="2412"/></proof>
7373
</goal>
7474
<goal name="binary_search&#39;vc.16" expl="postcondition" proved="true">
75-
<proof prover="1"><result status="valid" time="0.09" steps="756"/></proof>
75+
<proof prover="1"><result status="valid" time="0.09" steps="758"/></proof>
7676
</goal>
7777
<goal name="binary_search&#39;vc.17" expl="postcondition" proved="true">
78-
<proof prover="1"><result status="valid" time="0.32" steps="8288"/></proof>
78+
<proof prover="1"><result status="valid" time="0.32" steps="7799"/></proof>
7979
</goal>
8080
<goal name="binary_search&#39;vc.18" expl="postcondition" proved="true">
81-
<proof prover="1"><result status="valid" time="0.50" steps="11792"/></proof>
81+
<proof prover="1"><result status="valid" time="0.31" steps="7706"/></proof>
8282
</goal>
8383
</transf>
8484
</goal>

‎creusot/tests/should_succeed/binary_search/why3shapes.gz‎

-9 Bytes
Binary file not shown.

‎creusot/tests/should_succeed/bug/two_phase/why3session.xml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
<path name=".."/><path name="two_phase.mlcfg"/>
88
<theory name="TwoPhase_Test" proved="true">
99
<goal name="test&#39;vc" expl="VC for test" proved="true">
10-
<proof prover="1"><result status="valid" time="0.01" steps="36"/></proof>
10+
<proof prover="1"><result status="valid" time="0.01" steps="35"/></proof>
1111
</goal>
1212
</theory>
1313
</file>

‎creusot/tests/should_succeed/bug/two_phase/why3shapes.gz‎

-2 Bytes
Binary file not shown.

‎creusot/tests/should_succeed/cell/02/why3session.xml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@
3535
<proof prover="2"><result status="valid" time="0.01" steps="27"/></proof>
3636
</goal>
3737
<goal name="fib_memo&#39;vc.5" expl="integer overflow" proved="true">
38-
<proof prover="2"><result status="valid" time="0.01" steps="70"/></proof>
38+
<proof prover="2"><result status="valid" time="0.01" steps="69"/></proof>
3939
</goal>
4040
<goal name="fib_memo&#39;vc.6" expl="precondition" proved="true">
4141
<proof prover="2"><result status="valid" time="0.01" steps="32"/></proof>
@@ -47,19 +47,19 @@
4747
<proof prover="2"><result status="valid" time="0.01" steps="33"/></proof>
4848
</goal>
4949
<goal name="fib_memo&#39;vc.9" expl="integer overflow" proved="true">
50-
<proof prover="2"><result status="valid" time="0.09" steps="2037"/></proof>
50+
<proof prover="2"><result status="valid" time="0.09" steps="2829"/></proof>
5151
</goal>
5252
<goal name="fib_memo&#39;vc.10" expl="assertion" proved="true">
53-
<proof prover="1"><result status="valid" time="0.88" steps="72861"/></proof>
53+
<proof prover="1"><result status="valid" time="1.82" steps="181421"/></proof>
5454
</goal>
5555
<goal name="fib_memo&#39;vc.11" expl="precondition" proved="true">
5656
<proof prover="2"><result status="valid" time="0.01" steps="16"/></proof>
5757
</goal>
5858
<goal name="fib_memo&#39;vc.12" expl="precondition" proved="true">
59-
<proof prover="2"><result status="valid" time="0.02" steps="325"/></proof>
59+
<proof prover="2"><result status="valid" time="0.02" steps="324"/></proof>
6060
</goal>
6161
<goal name="fib_memo&#39;vc.13" expl="postcondition" proved="true">
62-
<proof prover="1"><result status="valid" time="0.09" steps="16025"/></proof>
62+
<proof prover="1"><result status="valid" time="0.09" steps="15818"/></proof>
6363
</goal>
6464
</transf>
6565
</goal>

‎creusot/tests/should_succeed/cell/02/why3shapes.gz‎

-12 Bytes
Binary file not shown.

‎creusot/tests/should_succeed/checked_ops/why3session.xml‎

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,12 @@
99
<path name=".."/><path name="checked_ops.mlcfg"/>
1010
<theory name="CheckedOps_TestU8AddExample" proved="true">
1111
<goal name="test_u8_add_example&#39;vc" expl="VC for test_u8_add_example" proved="true">
12-
<proof prover="0"><result status="valid" time="0.11" steps="29988"/></proof>
12+
<proof prover="0"><result status="valid" time="0.11" steps="26506"/></proof>
1313
</goal>
1414
</theory>
1515
<theory name="CheckedOps_TestU8AddOverflow" proved="true">
1616
<goal name="test_u8_add_overflow&#39;vc" expl="VC for test_u8_add_overflow" proved="true">
17-
<proof prover="0"><result status="valid" time="0.13" steps="25311"/></proof>
17+
<proof prover="0"><result status="valid" time="0.13" steps="22873"/></proof>
1818
</goal>
1919
</theory>
2020
<theory name="CheckedOps_TestU8WrappingAdd" proved="true">
@@ -24,17 +24,17 @@
2424
</theory>
2525
<theory name="CheckedOps_TestU8OverflowingAdd" proved="true">
2626
<goal name="test_u8_overflowing_add&#39;vc" expl="VC for test_u8_overflowing_add" proved="true">
27-
<proof prover="4"><result status="valid" time="0.01" steps="35"/></proof>
27+
<proof prover="4"><result status="valid" time="0.01" steps="31"/></proof>
2828
</goal>
2929
</theory>
3030
<theory name="CheckedOps_TestU8SubExample" proved="true">
3131
<goal name="test_u8_sub_example&#39;vc" expl="VC for test_u8_sub_example" proved="true">
32-
<proof prover="0"><result status="valid" time="0.10" steps="28982"/></proof>
32+
<proof prover="0"><result status="valid" time="0.10" steps="25704"/></proof>
3333
</goal>
3434
</theory>
3535
<theory name="CheckedOps_TestU8SubOverflow" proved="true">
3636
<goal name="test_u8_sub_overflow&#39;vc" expl="VC for test_u8_sub_overflow" proved="true">
37-
<proof prover="0"><result status="valid" time="0.15" steps="27701"/></proof>
37+
<proof prover="0"><result status="valid" time="0.15" steps="24820"/></proof>
3838
</goal>
3939
</theory>
4040
<theory name="CheckedOps_TestU8WrappingSub" proved="true">
@@ -44,22 +44,22 @@
4444
</theory>
4545
<theory name="CheckedOps_TestU8OverflowingSub" proved="true">
4646
<goal name="test_u8_overflowing_sub&#39;vc" expl="VC for test_u8_overflowing_sub" proved="true">
47-
<proof prover="4"><result status="valid" time="0.01" steps="35"/></proof>
47+
<proof prover="4"><result status="valid" time="0.01" steps="31"/></proof>
4848
</goal>
4949
</theory>
5050
<theory name="CheckedOps_TestU8MulExample" proved="true">
5151
<goal name="test_u8_mul_example&#39;vc" expl="VC for test_u8_mul_example" proved="true">
52-
<proof prover="0"><result status="valid" time="0.11" steps="29969"/></proof>
52+
<proof prover="0"><result status="valid" time="0.11" steps="26487"/></proof>
5353
</goal>
5454
</theory>
5555
<theory name="CheckedOps_TestU8MulZero" proved="true">
5656
<goal name="test_u8_mul_zero&#39;vc" expl="VC for test_u8_mul_zero" proved="true">
57-
<proof prover="4"><result status="valid" time="0.07" steps="2597"/></proof>
57+
<proof prover="4"><result status="valid" time="0.07" steps="2604"/></proof>
5858
</goal>
5959
</theory>
6060
<theory name="CheckedOps_TestU8OverflowingMul" proved="true">
6161
<goal name="test_u8_overflowing_mul&#39;vc" expl="VC for test_u8_overflowing_mul" proved="true">
62-
<proof prover="4"><result status="valid" time="0.01" steps="38"/></proof>
62+
<proof prover="4"><result status="valid" time="0.01" steps="34"/></proof>
6363
</goal>
6464
</theory>
6565
<theory name="CheckedOps_TestU8DivExample" proved="true">
@@ -69,27 +69,27 @@
6969
</theory>
7070
<theory name="CheckedOps_TestU8DivNoOverflow" proved="true">
7171
<goal name="test_u8_div_no_overflow&#39;vc" expl="VC for test_u8_div_no_overflow" proved="true">
72-
<proof prover="4"><result status="valid" time="0.05" steps="2134"/></proof>
72+
<proof prover="4"><result status="valid" time="0.05" steps="2714"/></proof>
7373
</goal>
7474
</theory>
7575
<theory name="CheckedOps_TestU8DivZero" proved="true">
7676
<goal name="test_u8_div_zero&#39;vc" expl="VC for test_u8_div_zero" proved="true">
77-
<proof prover="4"><result status="valid" time="0.00" steps="7"/></proof>
77+
<proof prover="4"><result status="valid" time="0.00" steps="2"/></proof>
7878
</goal>
7979
</theory>
8080
<theory name="CheckedOps_TestI8AddExample" proved="true">
8181
<goal name="test_i8_add_example&#39;vc" expl="VC for test_i8_add_example" proved="true">
82-
<proof prover="4"><result status="valid" time="0.18" steps="3079"/></proof>
82+
<proof prover="4"><result status="valid" time="0.18" steps="2968"/></proof>
8383
</goal>
8484
</theory>
8585
<theory name="CheckedOps_TestI8AddOverflowPos" proved="true">
8686
<goal name="test_i8_add_overflow_pos&#39;vc" expl="VC for test_i8_add_overflow_pos" proved="true">
87-
<proof prover="0"><result status="valid" time="0.15" steps="47115"/></proof>
87+
<proof prover="0"><result status="valid" time="0.15" steps="31877"/></proof>
8888
</goal>
8989
</theory>
9090
<theory name="CheckedOps_TestI8AddOverflowNeg" proved="true">
9191
<goal name="test_i8_add_overflow_neg&#39;vc" expl="VC for test_i8_add_overflow_neg" proved="true">
92-
<proof prover="0"><result status="valid" time="0.15" steps="27883"/></proof>
92+
<proof prover="0"><result status="valid" time="0.15" steps="24879"/></proof>
9393
</goal>
9494
</theory>
9595
<theory name="CheckedOps_TestI8WrappingAdd" proved="true">
@@ -99,22 +99,22 @@
9999
</theory>
100100
<theory name="CheckedOps_TestI8OverflowingAdd" proved="true">
101101
<goal name="test_i8_overflowing_add&#39;vc" expl="VC for test_i8_overflowing_add" proved="true">
102-
<proof prover="4"><result status="valid" time="0.01" steps="35"/></proof>
102+
<proof prover="4"><result status="valid" time="0.01" steps="32"/></proof>
103103
</goal>
104104
</theory>
105105
<theory name="CheckedOps_TestI8SubExample" proved="true">
106106
<goal name="test_i8_sub_example&#39;vc" expl="VC for test_i8_sub_example" proved="true">
107-
<proof prover="0"><result status="valid" time="0.14" steps="48418"/></proof>
107+
<proof prover="0"><result status="valid" time="0.14" steps="40267"/></proof>
108108
</goal>
109109
</theory>
110110
<theory name="CheckedOps_TestI8SubOverflowPos" proved="true">
111111
<goal name="test_i8_sub_overflow_pos&#39;vc" expl="VC for test_i8_sub_overflow_pos" proved="true">
112-
<proof prover="0"><result status="valid" time="0.16" steps="28349"/></proof>
112+
<proof prover="0"><result status="valid" time="0.16" steps="25094"/></proof>
113113
</goal>
114114
</theory>
115115
<theory name="CheckedOps_TestI8SubOverflowNeg" proved="true">
116116
<goal name="test_i8_sub_overflow_neg&#39;vc" expl="VC for test_i8_sub_overflow_neg" proved="true">
117-
<proof prover="0"><result status="valid" time="0.29" steps="79493"/></proof>
117+
<proof prover="0"><result status="valid" time="0.13" steps="35427"/></proof>
118118
</goal>
119119
</theory>
120120
<theory name="CheckedOps_TestI8WrappingSub" proved="true">
@@ -124,37 +124,37 @@
124124
</theory>
125125
<theory name="CheckedOps_TestI8OverflowingSub" proved="true">
126126
<goal name="test_i8_overflowing_sub&#39;vc" expl="VC for test_i8_overflowing_sub" proved="true">
127-
<proof prover="4"><result status="valid" time="0.01" steps="35"/></proof>
127+
<proof prover="4"><result status="valid" time="0.01" steps="32"/></proof>
128128
</goal>
129129
</theory>
130130
<theory name="CheckedOps_TestI8MulExample" proved="true">
131131
<goal name="test_i8_mul_example&#39;vc" expl="VC for test_i8_mul_example" proved="true">
132-
<proof prover="4"><result status="valid" time="0.10" steps="3370"/></proof>
132+
<proof prover="4"><result status="valid" time="0.10" steps="3277"/></proof>
133133
</goal>
134134
</theory>
135135
<theory name="CheckedOps_TestI8MulZero" proved="true">
136136
<goal name="test_i8_mul_zero&#39;vc" expl="VC for test_i8_mul_zero" proved="true">
137-
<proof prover="4"><result status="valid" time="0.32" steps="3257"/></proof>
137+
<proof prover="4"><result status="valid" time="0.32" steps="3392"/></proof>
138138
</goal>
139139
</theory>
140140
<theory name="CheckedOps_TestI8OverflowingMul" proved="true">
141141
<goal name="test_i8_overflowing_mul&#39;vc" expl="VC for test_i8_overflowing_mul" proved="true">
142-
<proof prover="4"><result status="valid" time="0.01" steps="38"/></proof>
142+
<proof prover="4"><result status="valid" time="0.01" steps="35"/></proof>
143143
</goal>
144144
</theory>
145145
<theory name="CheckedOps_TestI8DivExample" proved="true">
146146
<goal name="test_i8_div_example&#39;vc" expl="VC for test_i8_div_example" proved="true">
147-
<proof prover="4"><result status="valid" time="0.05" steps="522"/></proof>
147+
<proof prover="4"><result status="valid" time="0.05" steps="523"/></proof>
148148
</goal>
149149
</theory>
150150
<theory name="CheckedOps_TestI8DivNoOverflow" proved="true">
151151
<goal name="test_i8_div_no_overflow&#39;vc" expl="VC for test_i8_div_no_overflow" proved="true">
152-
<proof prover="1"><result status="valid" time="0.03" steps="48273"/></proof>
152+
<proof prover="1"><result status="valid" time="0.03" steps="116540"/></proof>
153153
</goal>
154154
</theory>
155155
<theory name="CheckedOps_TestI8DivZero" proved="true">
156156
<goal name="test_i8_div_zero&#39;vc" expl="VC for test_i8_div_zero" proved="true">
157-
<proof prover="4"><result status="valid" time="0.00" steps="7"/></proof>
157+
<proof prover="4"><result status="valid" time="0.00" steps="2"/></proof>
158158
</goal>
159159
</theory>
160160
</file>

‎creusot/tests/should_succeed/checked_ops/why3shapes.gz‎

-157 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)