
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 ?

