blob: f1cb8ff0129a25efc27bc02b9e34146630f16bfc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
% EXPECT: valid
% EXIT: 20
% Some tests from the CVC3 user manual.
% http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html
QUERY
( 0bin01@0bin0 = 0bin010 ) AND
( 0bin1000 >> 3 = 0bin0001 ) AND
( 0bin0011 << 3 = 0bin0011000 ) AND
( 0bin1000 >> 3 = 0bin0001 ) AND
TRUE
% these not working yet..
%( BVZEROEXTEND(0bin100, 5) = 0bin00100 ) AND
%( SX(0bin100, 5) = 0bin11100 ) AND
%
%( BVZEROEXTEND(0bin100, 3) = 0bin100 ) AND
%( SX(0bin100, 3) = 0bin100 )
;
|
