1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
-------------------- arrays.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
-------------------- bv0.bpl --------------------
bv0.bpl(4,3): Error: mismatched types in assignment command (cannot assign bv31 to bv32)
bv0.bpl(5,3): Error: mismatched types in assignment command (cannot assign int to bv32)
bv0.bpl(6,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)
bv0.bpl(7,10): Error: start index in extract must be no bigger than the end index
bv0.bpl(8,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)
bv0.bpl(9,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)
bv0.bpl(10,4): Error: mismatched types in assignment command (cannot assign concat$bvproxy#10 to bv32)
7 type checking errors detected in bv0.bpl
-------------------- bv1.bpl --------------------
Boogie program verifier finished with 1 verified, 0 errors
-------------------- bv2.bpl --------------------
bv2.bpl(4,13): Error: bitvector bounds in illegal position
bv2.bpl(6,13): Error: undeclared type: x
bv2.bpl(7,14): Error: bitvector bounds in illegal position
3 name resolution errors detected in bv2.bpl
-------------------- bv3.bpl --------------------
bv3.bpl(2,5): Error: type name: bv16 is registered for bitvectors
1 name resolution errors detected in bv3.bpl
-------------------- bv4.bpl --------------------
Boogie program verifier finished with 1 verified, 0 errors
-------------------- bv7.bpl --------------------
bv7.bpl(4,14): error: arguments of extract need to be integer literals
bv7.bpl(5,15): error: parentheses around bitvector bounds are not allowed
2 parse errors detected in bv7.bpl
-------------------- bv5.bpl --------------------
bv5.bpl(10,3): Error BP5001: This assertion might not hold.
Execution trace:
bv5.bpl(5,12): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- bv6.bpl --------------------
bv6.bpl(8,3): Error BP5001: This assertion might not hold.
Execution trace:
bv6.bpl(5,5): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- bv8.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
-------------------- bv10.bpl --------------------
Boogie program verifier finished with 1 verified, 0 errors
-------------------- bv9.bpl /proverOpt:OPTIMIZE_FOR_BV=true --------------------
Boogie program verifier finished with 1 verified, 0 errors
|
