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
|
% EXPECT: valid
% Some tests from the CVC3 user manual.
% http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html
x : BITVECTOR(5);
y : BITVECTOR(4);
yy : BITVECTOR(3);
bv : BITVECTOR(10);
a : BOOLEAN;
xx : BITVECTOR(8);
zz : BITVECTOR(12);
x4, y4 : BITVECTOR(4);
QUERY
( 0bin0000111101010000 = 0hex0f50 ) AND
( 0bin01@0bin0 = 0bin010 ) AND
( 0bin1000 >> 3 = 0bin0001 ) AND
( 0bin0011 << 3 = 0bin0011000 ) AND
( 0bin1000 >> 3 = 0bin0001 ) AND
( BVZEROEXTEND(0bin100, 2) = 0bin00100 ) AND
( SX(0bin100, 5) = 0bin11100 ) AND
( BVZEROEXTEND(0bin100, 0) = 0bin100 ) AND
( SX(0bin100, 3) = 0bin100 ) AND
( (BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11)))[8:4] = BVPLUS(5, x, ~(y[3:2])) ) AND
( x4 = 0hex5 AND y4 = 0bin0101 ) =>
( ( BVMULT(8,x4,y4)=BVMULT(8,y4,x4) ) AND
( NOT(BVLT(x4,y4)) ) AND
( BVLE(BVSUB(8,x4,y4), BVPLUS(8, x4, BVUMINUS(x4))) ) AND
( x4 = BVSUB(4, BVUMINUS(x4), BVPLUS(4, x4,0hex1)) ) ) AND
( 0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] ) AND
( 0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) = (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] ) AND
( xx = 0hexff AND zz = 0hexff0 =>
( zz = xx << 4 ) AND
( (zz >> 4)[7:0] = xx ) ) AND
TRUE;
|
