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

   1 x : BITVECTOR(5);
   2 y : BITVECTOR(4);
   3 yy : BITVECTOR(3);
   4
   5 % EXPECT: valid
   6 QUERY
   7  BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) ;