extern void abort(void);
#include <assert.h>
void reach_error() { assert(0); }

#include <stdlib.h>

extern int __VERIFIER_nondet_int(void);

/*
This source code is licensed under the GPLv3 license. 

Author: Alexander Driemeyer.
*/


struct data_struct {
  int number;
  int *array;
  int hasNextPartReference;
  struct data_struct *nextData;
};

typedef struct data_struct *Data;

struct node_t {
  Data data;
  struct node_t *next;
};

static Data create_data(Data prevData) {

  // create complex data

  if(prevData != NULL && prevData->hasNextPartReference) {
    return prevData->nextData;
  }

  Data data = malloc(sizeof *data);

  data->array = (int*) malloc(20 * sizeof(data->array));

  int counter = 0;
  for(counter = 0; counter < 20; counter++)  {
    data->array[counter] = __VERIFIER_nondet_int();
  }

  data->number = 0;
  int userInput = __VERIFIER_nondet_int();

  while(__VERIFIER_nondet_int() && data->number < 200 && data->number > -200 && userInput < 200 && userInput > -200) {
    data->number = data->number + __VERIFIER_nondet_int();
    userInput = __VERIFIER_nondet_int();
  }

  if(__VERIFIER_nondet_int()) {

    Data nextData = malloc(sizeof *data);
    nextData->array = NULL;

    nextData->number = data->number - 200;
    data->number = 200;
    data->hasNextPartReference = 1;
    data->nextData = nextData;

    // assigned wrong variable
    data->hasNextPartReference = 0;
    data->nextData = NULL;
  } else {
    data->hasNextPartReference = 0;
    data->nextData = NULL;
  }

  return data;
}

static void freeData(Data data) {
  free(data->array);
  free(data);
}

static void append(struct node_t **pointerToList) {
  struct node_t *node = malloc(sizeof *node);
  node->next = *pointerToList;

  if(*pointerToList == NULL) {
    node->data = create_data(NULL);
  } else {
    node->data = create_data(node->next->data);
  }

  *pointerToList = node;
}

int main() {
  struct node_t *list = NULL;

  /* Create a long singly-linked list with complex data.

     Data of a list segment may contain reference to
     data of the next list segment, but no more than
     two data segments may be linked together.
     However, the data itself does not matter when verifying this program.
  */

  int dataNotFinished = 0;

  do {
    append(&list);
    dataNotFinished = list->data != NULL && list->data->hasNextPartReference;
  } while(dataNotFinished ||  __VERIFIER_nondet_int());

/*
Do something with data.
  displayData();
*/

//  free list and data
  while (list) {
    struct node_t *next = list->next;
    freeData(list->data);
    free(list);
    list = next;
  }

  return 0;
}