./deagle /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c --64


--------------------------------------------------------------------------------


./deagle_exe --svcomp --graphml-witness error-witness.graphml --no-assertions --datarace /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c
Deagle version 2.2 64-bit x86_64 linux
which contains:
CBMC version 5.67.0 (svcomp24-11-gfd1b965b5-dirty) 64-bit x86_64 linux
Parsing /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_cond_init> line 7: 
reason for conflict at #this.__data: names of member 0 differ (__annonCompField1/__wseq)

struct __pthread_cond_s {
  union __anonunion____missing_field_name_419937108 __annonCompField1;
  union __anonunion____missing_field_name_845759682 __annonCompField2;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
struct __pthread_cond_s {
  __atomic_wide_counter __wseq;
  __atomic_wide_counter __g1_start;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
warning: pointer parameter types differ between declaration and definition "pthread_cond_init"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 8799
signed int (pthread_cond_t *, const pthread_condattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_init> line 7
signed int (pthread_cond_t *cond, const pthread_condattr_t *attr)
file <builtin-library-pthread_mutex_unlock> line 17: warning: pointer parameter types differ between declaration and definition "pthread_mutex_unlock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 8798
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_unlock> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-pthread_mutex_lock> line 17: warning: pointer parameter types differ between declaration and definition "pthread_mutex_lock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 8797
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_lock> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-pthread_mutex_destroy> line 17: warning: pointer parameter types differ between declaration and definition "pthread_mutex_destroy"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 8796
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_destroy> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-pthread_mutex_init> line 27: warning: pointer parameter types differ between declaration and definition "pthread_mutex_init"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 8794
signed int (pthread_mutex_t *, const pthread_mutexattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_init> line 27
signed int (pthread_mutex_t *mutex, const pthread_mutexattr_t *mutexattr)
file <builtin-library-__sigsetjmp> line 9: 
reason for conflict at #this: number of members is different (3/4)

struct __jmp_buf_tag {
  __jmp_buf __jmpbuf;
  signed int __mask_was_saved;
  __sigset_t __saved_mask;
}
struct __jmp_buf_tag {
  __jmp_buf __jmpbuf;
  signed int __mask_was_saved;
  __sigset_t __saved_mask;
  unsigned int $pad3;
}
warning: pointer parameter types differ between declaration and definition "__sigsetjmp"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 8792
signed int (struct __jmp_buf_tag *, signed int)
new definition in module <built-in-library> file <builtin-library-__sigsetjmp> line 9
signed int (struct __jmp_buf_tag *env, signed int savesigs)
file <builtin-library-pthread_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 8778
signed int (pthread_t *, const pthread_attr_t *, void * (*)(void *), void *)
new definition in module <built-in-library> file <builtin-library-pthread_create> line 20
signed int (pthread_t *pthread_create$$thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
file <builtin-library-localtime> line 9: warning: conflicting return types "localtime"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 425
struct tm * (const time_t *)
new definition in module <built-in-library> file <builtin-library-localtime> line 9
struct tm * (const time_t *clock)
file <builtin-library-localtime> line 9: 
reason for conflict at #this: names of member 9 differ (__tm_gmtoff/tm_gmtoff)

struct tm {
  signed int tm_sec;
  signed int tm_min;
  signed int tm_hour;
  signed int tm_mday;
  signed int tm_mon;
  signed int tm_year;
  signed int tm_wday;
  signed int tm_yday;
  signed int tm_isdst;
  signed long int __tm_gmtoff;
  const char * __tm_zone;
}
struct tm {
  signed int tm_sec;
  signed int tm_min;
  signed int tm_hour;
  signed int tm_mday;
  signed int tm_mon;
  signed int tm_year;
  signed int tm_wday;
  signed int tm_yday;
  signed int tm_isdst;
  signed long int tm_gmtoff;
  const char * tm_zone;
}
warning: pointer parameter types differ between declaration and definition "localtime"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 425
struct tm * (const time_t *)
new definition in module <built-in-library> file <builtin-library-localtime> line 9
struct tm * (const time_t *clock)
file <builtin-library-fputs> line 9: 
reason for conflict at #this._chain->_old_offset: conflict on POD

__off_t
__off_t

reason for conflict at #this._chain->_old_offset: type of member _chain differs (recursive)

struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
warning: pointer parameter types differ between declaration and definition "fputs"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 387
signed int (const char *, FILE *)
new definition in module <built-in-library> file <builtin-library-fputs> line 9
signed int (const char *s, FILE *stream)
file <builtin-library-vfprintf> line 14: 
reason for conflict at #this._chain->_old_offset: conflict on POD

__off_t
__off_t

reason for conflict at #this._chain->_old_offset: type of member _chain differs (recursive)

struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
warning: pointer parameter types differ between declaration and definition "vfprintf"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 383
signed int (FILE *, const char *, __gnuc_va_list)
new definition in module <built-in-library> file <builtin-library-vfprintf> line 14
signed int (FILE *stream, const char * restrict format, va_list arg)
file /usr/include/stdio.h line 144: warning: conflicting pointer types for variable "stdout"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 377
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
} *
new definition in module <built-in-library> file /usr/include/stdio.h line 144
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
} *
file <builtin-library-longjmp> line 7: 
reason for conflict at #this: number of members is different (3/4)

struct __jmp_buf_tag {
  __jmp_buf __jmpbuf;
  signed int __mask_was_saved;
  __sigset_t __saved_mask;
}
struct __jmp_buf_tag {
  __jmp_buf __jmpbuf;
  signed int __mask_was_saved;
  __sigset_t __saved_mask;
  unsigned int $pad3;
}
warning: pointer parameter types differ between declaration and definition "longjmp"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 492
_Noreturn void (struct __jmp_buf_tag *, signed int)
new definition in module <built-in-library> file <builtin-library-longjmp> line 7
void (struct __jmp_buf_tag *env, signed int val)
file <builtin-library-pthread_cond_wait> line 7: 
reason for conflict at #this.__data: names of member 0 differ (__annonCompField1/__wseq)

struct __pthread_cond_s {
  union __anonunion____missing_field_name_419937108 __annonCompField1;
  union __anonunion____missing_field_name_845759682 __annonCompField2;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
struct __pthread_cond_s {
  __atomic_wide_counter __wseq;
  __atomic_wide_counter __g1_start;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
warning: pointer parameter types differ between declaration and definition "pthread_cond_wait"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 8803
signed int (pthread_cond_t *, pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_wait> line 7
signed int (pthread_cond_t *cond, pthread_mutex_t *mutex)
file <builtin-library-_setjmp> line 7: 
reason for conflict at #this: number of members is different (3/4)

struct __jmp_buf_tag {
  __jmp_buf __jmpbuf;
  signed int __mask_was_saved;
  __sigset_t __saved_mask;
}
struct __jmp_buf_tag {
  __jmp_buf __jmpbuf;
  signed int __mask_was_saved;
  __sigset_t __saved_mask;
  unsigned int $pad3;
}
warning: pointer parameter types differ between declaration and definition "_setjmp"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 491
signed int (struct __jmp_buf_tag *)
new definition in module <built-in-library> file <builtin-library-_setjmp> line 7
signed int (struct __jmp_buf_tag *env)
file <builtin-library-mktime> line 11: warning: conflicting return types "mktime"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 424
time_t (struct tm *)
new definition in module <built-in-library> file <builtin-library-mktime> line 11
time_t (struct tm *timeptr)
file <builtin-library-mktime> line 11: 
reason for conflict at #this: conflict on POD

time_t
time_t
error: conflicting function declarations 'mktime'
old definition in module 'main' file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 424
time_t (struct tm *)
new definition in module '<built-in-library>' file <builtin-library-mktime> line 11
time_t (struct tm *timeptr)
file <builtin-library-fprintf> line 12: 
reason for conflict at #this._chain->_old_offset: conflict on POD

__off_t
__off_t

reason for conflict at #this._chain->_old_offset: type of member _chain differs (recursive)

struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
warning: pointer parameter types differ between declaration and definition "fprintf"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 380
signed int (FILE *, const char *, ...)
new definition in module <built-in-library> file <builtin-library-fprintf> line 12
signed int (FILE *stream, const char * restrict format, ...)
file <builtin-library-time> line 11: warning: conflicting return types "time"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 423
time_t (time_t *)
new definition in module <built-in-library> file <builtin-library-time> line 11
time_t (time_t *tloc)
file <builtin-library-time> line 11: 
reason for conflict at #this: conflict on POD

time_t
time_t
error: conflicting function declarations 'time'
old definition in module 'main' file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 423
time_t (time_t *)
new definition in module '<built-in-library>' file <builtin-library-time> line 11
time_t (time_t *tloc)
file /usr/include/stdio.h line 145: warning: conflicting pointer types for variable "stderr"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 378
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
} *
new definition in module <built-in-library> file /usr/include/stdio.h line 145
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
} *
file <builtin-library-fflush> line 9: 
reason for conflict at #this._chain->_old_offset: conflict on POD

__off_t
__off_t

reason for conflict at #this._chain->_old_offset: type of member _chain differs (recursive)

struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
warning: pointer parameter types differ between declaration and definition "fflush"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 379
signed int (FILE *)
new definition in module <built-in-library> file <builtin-library-fflush> line 9
signed int (FILE *stream)
file <builtin-library-pthread_cond_broadcast> line 7: 
reason for conflict at #this.__data: names of member 0 differ (__annonCompField1/__wseq)

struct __pthread_cond_s {
  union __anonunion____missing_field_name_419937108 __annonCompField1;
  union __anonunion____missing_field_name_845759682 __annonCompField2;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
struct __pthread_cond_s {
  __atomic_wide_counter __wseq;
  __atomic_wide_counter __g1_start;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
warning: pointer parameter types differ between declaration and definition "pthread_cond_broadcast"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 8802
signed int (pthread_cond_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_broadcast> line 7
signed int (pthread_cond_t *cond)
file <builtin-library-ctime> line 7: 
reason for conflict at #this: conflict on POD

const time_t
const time_t
warning: pointer parameter types differ between declaration and definition "ctime"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 426
char * (const time_t *)
new definition in module <built-in-library> file <builtin-library-ctime> line 7
char * (const time_t *clock)
Removal of function pointers and virtual functions
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 9188 function join_: replacing function pointer by 10 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 9226 function join_all_: replacing function pointer by 10 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 9025 function free_lock_: replacing function pointer by 10 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 8843 function fail: replacing function pointer by 10 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 8865 function my_malloc: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 9068 function reenter: replacing function pointer by 10 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 9092 function ignition: replacing function pointer by 10 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 9097 function ignition: replacing function pointer by 10 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/pigz/main.c line 9104 function ignition: replacing function pointer by 10 possible targets
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 10 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
argc''s upper bound is 1073741824
getchar::1::return_value's upper bound is 255
set limit type 2
too many unwind!
