array_ptr_single_elem_init_true-unreach-call.i

typedef unsigned int size_t;
extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
extern int __VERIFIER_nondet_int(void);
void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } }
struct S
{
 int *p;
 int n;
};
struct S *a[100000];
int main()
{
 int i;
 for (i = 0; i < 100000; i++)
 {
  int q = __VERIFIER_nondet_int();
  struct S *s = (void *)0;
  if (q == 0)
  {
   s = (struct S*) malloc(sizeof(struct S));
   s->n = q % 2;
  }
  if (s != 0)
  {
   if (s->n == 0)
   {
    s->p = (int *) malloc(sizeof(int));
   }
   else
   {
    s->p = (void *)0;
   }
  }
  a[i] = s;
 }
 a[3] = (struct S*) malloc(sizeof(struct S));
 for (i = 0; i < 100000; i++)
 {
  struct S *s1 = a[i];
  if (i != 3 && s1 != (void *)0 && s1->n == 0)
  {
   __VERIFIER_assert(s1->p != (void *)0);
  }
 }
 return 0;
}