test/regress/regress0/cvc3.userdoc.01.cvc


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

% COMMAND-LINE: --incremental

% EXPECT: entailed
QUERY 0bin0000111101010000  = 0hex0f50;

% EXPECT: entailed
QUERY 0bin01@0bin0          = 0bin010;

% EXPECT: entailed
QUERY 0bin0011[3:1]         = 0bin001;

% EXPECT: entailed
QUERY 0bin0011 << 3         = 0bin0011000;

% EXPECT: entailed
QUERY 0bin1000 >> 3         = 0bin0001;

% EXPECT: entailed
QUERY SX(0bin100, 5)        = 0bin11100;

% EXPECT: entailed
QUERY BVZEROEXTEND(0bin1,3) = 0bin0001;

% EXPECT: entailed
QUERY BVREPEAT(0bin10,3)    = 0bin101010;

% EXPECT: entailed
QUERY BVROTL(0bin101,1)     = 0bin011;

% EXPECT: entailed
QUERY BVROTR(0bin101,1)     = 0bin110;