struct obj {
     char values[100000];
     struct {
         int a: 1;
         int b: 3;
     };
 };
 union byte {
     struct obj o;
     char bytes[100000];
 };
 void init_obj(struct obj *o) {
     for(int i = 0; i < 8; i++)
         o->values[i] = nondet_int();
 }
 union byte u;
 int main() {
     init_obj(&u.o);
     u.bytes[1] = 3;
      __ESBMC_init_object(u.bytes);
     __ESBMC_assert(u.bytes[10000] == 3 , "asd");

 }