This project is read-only.

the question of Bitvector Reasoning in vcc

Mar 23, 2015 at 9:37 AM
recently ,I am learning the VCC tutorial . In 2.4.1 of the tutorial,there is a example about the bitvector Reasoning.
   #include <vcc.h>
   int min(int a, int b)
      _(requires \true)
      _(ensures \result <= a && \result <= b)
 {
      _(assert {:bv} \forall int x; (x & (-1)) == x)
      _(assert {:bv} \forall int a,b; (a - (a - b)) == b)
      return _(unchecked)(a - ((a - b) & -(a > b)));
 }
I think, in this example ,the contract "\forall int x; (x & (-1)) == x" and "\forall int x; (x & (0)) == 0" have the same status. but when I delete " _(assert {:bv} \forall int x; (x & (-1)) == x)",the VCC report " error VC9501: Post condition '\result <= a && \result <= b' did not verify" . why does the assert "\forall int x; (x & (0)) == 0" can be omited , but "_(assert {:bv} \forall int x; (x & (-1)) == x)" cant ?

could anyone help me ?