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

   1 x, y : BITVECTOR(4);
   2
   3 ASSERT x = 0hex5;
   4 ASSERT y = 0bin0101;
   5
   6 % EXPECT: entailed
   7 QUERY
   8  BVMULT(8,x,y)=BVMULT(8,y,x)
   9  AND
  10  NOT(BVLT(x,y))
  11  AND
  12  BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x)))
  13  AND
  14  x = BVSUB(4, BVUMINUS(x), BVPLUS(4, x,0hex1)) ;