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

   1 % COMMAND-LINE: --incremental
   2
   3 % EXPECT: entailed
   4 QUERY 0bin0000111101010000  = 0hex0f50;
   5
   6 % EXPECT: entailed
   7 QUERY 0bin01@0bin0          = 0bin010;
   8
   9 % EXPECT: entailed
  10 QUERY 0bin0011[3:1]         = 0bin001;
  11
  12 % EXPECT: entailed
  13 QUERY 0bin0011 << 3         = 0bin0011000;
  14
  15 % EXPECT: entailed
  16 QUERY 0bin1000 >> 3         = 0bin0001;
  17
  18 % EXPECT: entailed
  19 QUERY SX(0bin100, 5)        = 0bin11100;
  20
  21 % EXPECT: entailed
  22 QUERY BVZEROEXTEND(0bin1,3) = 0bin0001;
  23
  24 % EXPECT: entailed
  25 QUERY BVREPEAT(0bin10,3)    = 0bin101010;
  26
  27 % EXPECT: entailed
  28 QUERY BVROTL(0bin101,1)     = 0bin011;
  29
  30 % EXPECT: entailed
  31 QUERY BVROTR(0bin101,1)     = 0bin110;