Проверка модели CBMC

Question

Я пытаюсь ограничить стол b[4][4] такой, что только те места, которые имеют i>=j и удовлетворяя условию, что (stored[i] & stored[j]) == stored[i] будет 1, а остальные будут 0.

Почему это не работает?

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])));  
      }
   }

Предположим, что пытаемся получить эффект, который b[i][j] == 1 должно подразумевать stored[i]& stored[j] == stored[i], Но вывод не имеет этого эффекта. В чем проблема? Я новичок в CBMC и C также.

Answer 1

Обратите внимание, что значения в bitvector stored[4] = {111,001,010,000}; находятся в базе 10.

Вы имеете в виду базу 2 {0b111,0b001,0b010,0b000}?