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


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


./deagle_exe --svcomp --graphml-witness error-witness.graphml --no-assertions --datarace /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/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/phpspy/main.c
Converting
Type-checking main
Generating GOTO Program
doing sscanf! arguments include:
typecast
  * type: pointer
      * #source_location: 
        * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
        * line: 3891
        * function: update_term_size_via_esc
        * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
      * width: 32
      * #restricted: 1
      0: signedbv
          * width: 8
          * #constant: 1
          * #c_type: char
  * #source_location: 
    * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
    * line: 3891
    * function: update_term_size_via_esc
    * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
  0: address_of
      * type: pointer
          * width: 32
          0: signedbv
              * width: 8
              * #c_type: char
      0: index
          * type: signedbv
              * width: 8
              * #c_type: char
          0: symbol
              * type: array
                  * #source_location: 
                    * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
                    * line: 3849
                    * function: update_term_size_via_esc
                    * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
                  * #index_type: signedbv
                      * width: 32
                      * #c_type: signed_int
                  * size: constant
                      * type: signedbv
                          * width: 32
                          * #c_type: signed_int
                      * #source_location: 
                        * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
                        * line: 3849
                        * function: update_term_size_via_esc
                        * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
                      * value: 40
                      * #base: 10
                  0: signedbv
                      * width: 8
                      * #c_type: char
              * #source_location: 
                * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
                * line: 3891
                * function: update_term_size_via_esc
                * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
              * identifier: update_term_size_via_esc::1::buf___0
              * #lvalue: 1
          1: constant
              * type: signedbv
                  * width: 32
                  * #c_type: signed_int
              * value: 0
typecast
  * type: pointer
      * #source_location: 
        * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
        * line: 3891
        * function: update_term_size_via_esc
        * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
      * width: 32
      * #restricted: 1
      0: signedbv
          * width: 8
          * #constant: 1
          * #c_type: char
  * #source_location: 
    * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
    * line: 3891
    * function: update_term_size_via_esc
    * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
  0: address_of
      * type: pointer
          * width: 32
          0: signedbv
              * width: 8
              * #c_type: char
      0: index
          * type: signedbv
              * width: 8
              * #c_type: char
          0: string_constant
              * type: array
                  * size: constant
                      * type: signedbv
                          * width: 32
                          * #c_type: signed_int
                      * value: 9
                  0: signedbv
                      * width: 8
                      * #c_type: char
              * #source_location: 
                * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
                * line: 3891
                * function: update_term_size_via_esc
                * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
              * value: [%d;%dR
              * #lvalue: 1
          1: constant
              * type: signedbv
                  * width: 32
                  * #c_type: signed_int
              * value: 0
address_of
  * type: pointer
      * width: 32
      0: signedbv
          * width: 32
          * #c_type: signed_int
  * #source_location: 
    * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
    * line: 3892
    * function: update_term_size_via_esc
    * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
  0: symbol
      * type: signedbv
          * width: 32
          * #c_type: signed_int
      * #source_location: 
        * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
        * line: 3892
        * function: update_term_size_via_esc
        * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
      * identifier: update_term_size_via_esc::1::rh
      * #lvalue: 1
address_of
  * type: pointer
      * width: 32
      0: signedbv
          * width: 32
          * #c_type: signed_int
  * #source_location: 
    * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
    * line: 3892
    * function: update_term_size_via_esc
    * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
  0: symbol
      * type: signedbv
          * width: 32
          * #c_type: signed_int
      * #source_location: 
        * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c
        * line: 3892
        * function: update_term_size_via_esc
        * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
      * identifier: update_term_size_via_esc::1::rw
      * #lvalue: 1
Adding CPROVER library (x86_64)
file <builtin-library-fgets> line 10: 
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 "fgets"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 16255
char * (char *, signed int, FILE *)
new definition in module <built-in-library> file <builtin-library-fgets> line 10
char * (char *str, signed int size, FILE *stream)
file <builtin-library-pthread_cond_signal> line 7: 
reason for conflict at #this.__data: names of member 0 differ (__annonCompField1/__wseq)

struct __pthread_cond_s {
  union __anonunion____missing_field_name_419419941 __annonCompField1;
  union __anonunion____missing_field_name_349613679 __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_signal"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 16247
signed int (pthread_cond_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_signal> line 7
signed int (pthread_cond_t *cond)
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/phpspy/main.c line 16243
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 *pthread_mutex_unlock$$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/phpspy/main.c line 16242
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 *pthread_mutex_lock$$mutex)
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/phpspy/main.c line 1603
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 <builtin-library-fclose> 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 "fclose"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 1598
signed int (FILE *)
new definition in module <built-in-library> file <builtin-library-fclose> line 14
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_419419941 __annonCompField1;
  union __anonunion____missing_field_name_349613679 __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/phpspy/main.c line 16248
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-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/phpspy/main.c line 16234
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 *thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
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/phpspy/main.c line 16241
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 *pthread_mutex_destroy$$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/phpspy/main.c line 16239
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 *pthread_mutex_init$$mutex, const pthread_mutexattr_t *mutexattr)
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_419419941 __annonCompField1;
  union __anonunion____missing_field_name_349613679 __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/phpspy/main.c line 16244
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-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/phpspy/main.c line 1600
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-fdopen> line 12: warning: conflicting return types "fdopen"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 18193
FILE * (signed int, const char *)
new definition in module <built-in-library> file <builtin-library-fdopen> line 12
FILE * (signed int handle, const char *mode)
file <builtin-library-fdopen> 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 "fdopen"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 18193
FILE * (signed int, const char *)
new definition in module <built-in-library> file <builtin-library-fdopen> line 12
FILE * (signed int handle, const char *mode)
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/phpspy/main.c line 1596
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 /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/phpspy/main.c line 1597
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-fileno> 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 "fileno"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 1639
signed int (FILE *)
new definition in module <built-in-library> file <builtin-library-fileno> line 9
signed int (FILE *stream)
file <builtin-library-fopen> line 15: warning: conflicting return types "fopen"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 1599
FILE * (const char *, const char *)
new definition in module <built-in-library> file <builtin-library-fopen> line 15
FILE * (const char *filename, const char *mode)
file <builtin-library-fopen> line 15: 
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 "fopen"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 1599
FILE * (const char *, const char *)
new definition in module <built-in-library> file <builtin-library-fopen> line 15
FILE * (const char *filename, const char *mode)
file <builtin-library-fread> line 10: 
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 "fread"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 1635
size_t (void *, size_t, size_t, FILE *)
new definition in module <built-in-library> file <builtin-library-fread> line 10
size_t (void *ptr, size_t size, size_t nitems, FILE *stream)
Removal of function pointers and virtual functions
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 6028 function main_pid: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 6103 function main_pid: replacing function pointer by 9 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 6134 function main_pid: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 4500 function extract_esc_user: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 8097 function do_trace_70: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 8183 function do_trace_70: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 9265 function do_trace_71: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 9351 function do_trace_71: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 10433 function do_trace_72: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 10519 function do_trace_72: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 11601 function do_trace_73: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 11687 function do_trace_73: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 12769 function do_trace_74: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 12855 function do_trace_74: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 13937 function do_trace_80: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 14023 function do_trace_80: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 15105 function do_trace_81: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 15191 function do_trace_81: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 8308 function trace_stack_70: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 8425 function trace_request_info_70: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 8464 function trace_memory_info_70: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 8513 function trace_globals_70: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 8911 function trace_locals_70: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 9476 function trace_stack_71: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 9593 function trace_request_info_71: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 9632 function trace_memory_info_71: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 9681 function trace_globals_71: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 10079 function trace_locals_71: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 10644 function trace_stack_72: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 10761 function trace_request_info_72: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 10800 function trace_memory_info_72: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 10849 function trace_globals_72: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 11247 function trace_locals_72: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 11812 function trace_stack_73: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 11929 function trace_request_info_73: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 11968 function trace_memory_info_73: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 12017 function trace_globals_73: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 12415 function trace_locals_73: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 12980 function trace_stack_74: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 13097 function trace_request_info_74: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 13136 function trace_memory_info_74: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 13185 function trace_globals_74: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 13583 function trace_locals_74: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 14148 function trace_stack_80: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 14265 function trace_request_info_80: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 14304 function trace_memory_info_80: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 14353 function trace_globals_80: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 14751 function trace_locals_80: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 15316 function trace_stack_81: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 15433 function trace_request_info_81: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 15472 function trace_memory_info_81: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 15521 function trace_globals_81: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 15919 function trace_locals_81: replacing function pointer by 3 possible targets
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 11 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
argc''s upper bound is 1073741824
set limit type 2
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
**** WARNING: no body for function fork
**** WARNING: no body for function strstr
**** WARNING: no body for function getpid
**** WARNING: no body for function asprintf
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function dup2
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function ptrace
**** WARNING: no body for function execvp
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function waitpid
**** WARNING: no body for function vsnprintf
**** WARNING: no body for function popen
**** WARNING: no body for function pclose
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
Unwinding loop popen_read_line.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Not unwinding loop popen_read_line.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
**** WARNING: no body for function snprintf
**** WARNING: no body for function access
Unwinding loop strcpy.0 iteration 1 file <builtin-library-strcpy> line 32 function strcpy thread 0
Not unwinding loop strcpy.0 iteration 2 file <builtin-library-strcpy> line 32 function strcpy thread 0
Unwinding loop shell_escape.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17572 function shell_escape thread 0
Not unwinding loop shell_escape.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17572 function shell_escape thread 0
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
Unwinding loop popen_read_line.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Not unwinding loop popen_read_line.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
**** WARNING: no body for function strtoull
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
Unwinding loop popen_read_line.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Not unwinding loop popen_read_line.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
Unwinding loop popen_read_line.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Not unwinding loop popen_read_line.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
Unwinding loop popen_read_line.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Not unwinding loop popen_read_line.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Unwinding loop strcpy.0 iteration 1 file <builtin-library-strcpy> line 32 function strcpy thread 0
Not unwinding loop strcpy.0 iteration 2 file <builtin-library-strcpy> line 32 function strcpy thread 0
Unwinding loop shell_escape.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17572 function shell_escape thread 0
Not unwinding loop shell_escape.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17572 function shell_escape thread 0
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
Unwinding loop popen_read_line.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Not unwinding loop popen_read_line.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
Unwinding loop popen_read_line.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Not unwinding loop popen_read_line.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
Unwinding loop popen_read_line.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Not unwinding loop popen_read_line.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/phpspy/main.c line 17789 function popen_read_line thread 0
Unwinding loop strcmp.0 iteration 1 file <builtin-library-strcmp> line 44 function strcmp thread 0
**** WARNING: no body for function dup
Unwinding loop strcmp.0 iteration 1 file <builtin-library-strcmp> line 44 function strcmp thread 0
Not unwinding loop strcmp.0 iteration 2 file <builtin-library-strcmp> line 44 function strcmp thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
Start removing dummy accesses: 8511 steps before removal
8511 steps after removal
Handling datarace with no aid
The number of races before filter: 0
The number of races after filter: 0
The number of race categories before filter: 0
The number of race categories after filter: 0
Runtime Symex: 1.29381s
size of program expression: 8511 steps
simple slicing removed 3079 assignments
Generated 10 VCC(s), 8 remaining after simplification
Runtime Postprocess Equation: 0.00150391s
Passing problem to propositional reduction
converting SSA
too many addressed objects: maximum number of objects is set to 2^n=256 (with n=8); use the `--object-bits n` option to increase the maximum number
