summaryrefslogtreecommitdiff
path: root/test/regress/regress0/cvc3.userdoc.06.cvc
blob: 3968365ad84e683a447e764015080a7a444d69c0 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13

% COMMAND-LINE: --incremental

x, y : BITVECTOR(8);
z, t : BITVECTOR(12);

ASSERT x = 0hexff;
ASSERT z = 0hexff0;

% EXPECT: entailed
QUERY  z = x << 4;

% EXPECT: entailed
QUERY (z >> 4)[7:0] = x;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback