blob: 50c33cc3c9cc317a7b63d95726af1c37dbca349f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
// RUN: %boogie -proverWarnings:1 %s > %t
// RUN: %diff %s.expect %t
procedure foo(x : bv32) returns(r : bv32)
{
var q : bv64;
block1:
r := 17bv32;
assert r == r;
assert r[32:0] == r[32:0];
assert 0bv2 ++ r[12:0] == 0bv2 ++ r[12:0];
r := 17bv10 ++ 17bv22;
// r := 17;
q := 420000000000bv64;
q := 8444249301319680000bv64;
q := 16444249301319680000bv64;
return;
}
|