CBMC Model Checking

Question

I'm trying to constraint the table b[4][4] such that only those places which have i>=j and satisfying the condition that (stored[i] & stored[j]) == stored[i] be 1, and the rest be 0.

Why this is not working?

void main(){
  unsigned int i = 0  , j = 0; 
  _Bool b[4][4];
  bitvector stored[4] = {111,001,010,000};
  for(i=0;i<4;i++){
     for(j=0;j<4;j++){
      __CPROVER_assume( !(b[i][j]) || ((i>=j) && (stored[i] & stored[j] == stored[i])));  
      }
   }

CProver assume trying to get an effect that b[i][j] == 1 should imply stored[i]& stored[j] == stored[i]. But the output doesn't have this effect. What's the problem? I'm new to CBMC and to C also.

Answer 1

Note that values in bitvector stored[4] = {111,001,010,000}; are in base 10.

Do you mean base 2 {0b111,0b001,0b010,0b000}?