array_of_struct_single_elem_init_true-unreach-call.i

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;
  if (s.n == 0)
  {
      s.p =10 ;
  }
  else
  {
    s.p = 20;
  }
  a[i] = s;
 }
 a[3].p = 30;
 a[3].n = 40;
 for (i = 0; i < 100000; i++)
 {
  struct S s1 = a[i];
  if (i != 3 && s1.n == 0)
  {
   __VERIFIER_assert(s1.p == 10);
  }
 }
 return 0;
}