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


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


./deagle_exe --svcomp --graphml-witness error-witness.graphml --no-assertions --datarace /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/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/dnspod-sr/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/dnspod-sr/main.c
        * line: 6318
        * function: read_resolve
        * 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/dnspod-sr/main.c
    * line: 6318
    * function: read_resolve
    * 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/dnspod-sr/main.c
                    * line: 6259
                    * function: read_resolve
                    * 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/dnspod-sr/main.c
                        * line: 6259
                        * function: read_resolve
                        * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
                      * value: 400
                      * #base: 10
                  0: signedbv
                      * width: 8
                      * #c_type: char
              * #source_location: 
                * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
                * line: 6318
                * function: read_resolve
                * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
              * identifier: read_resolve::1::buf
              * #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/dnspod-sr/main.c
        * line: 6318
        * function: read_resolve
        * 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/dnspod-sr/main.c
    * line: 6318
    * function: read_resolve
    * 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: 6
                  0: signedbv
                      * width: 8
                      * #c_type: char
              * #source_location: 
                * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
                * line: 6318
                * function: read_resolve
                * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
              * value: %s %s
              * #lvalue: 1
          1: constant
              * type: signedbv
                  * width: 32
                  * #c_type: signed_int
              * value: 0
typecast
  * type: pointer
      * width: 32
      0: empty
          * #constant: 1
  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/dnspod-sr/main.c
                    * line: 6263
                    * function: read_resolve
                    * 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/dnspod-sr/main.c
                        * line: 6263
                        * function: read_resolve
                        * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
                      * value: 80
                      * #base: 10
                  0: signedbv
                      * width: 8
                      * #c_type: char
              * #source_location: 
                * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
                * line: 6319
                * function: read_resolve
                * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
              * identifier: read_resolve::1::placeholder
              * #lvalue: 1
          1: constant
              * type: signedbv
                  * width: 32
                  * #c_type: signed_int
              * value: 0
typecast
  * type: pointer
      * width: 32
      0: empty
          * #constant: 1
  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/dnspod-sr/main.c
                    * line: 6265
                    * function: read_resolve
                    * 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/dnspod-sr/main.c
                        * line: 6265
                        * function: read_resolve
                        * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
                      * value: 20
                      * #base: 10
                  0: signedbv
                      * width: 8
                      * #c_type: char
              * #source_location: 
                * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
                * line: 6319
                * function: read_resolve
                * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
              * identifier: read_resolve::1::temp
              * #lvalue: 1
          1: constant
              * type: signedbv
                  * width: 32
                  * #c_type: signed_int
              * value: 0
doing sscanf! arguments include:
typecast
  * type: pointer
      * #source_location: 
        * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
        * line: 9112
        * function: cmd_analyze
        * 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/dnspod-sr/main.c
    * line: 9112
    * function: cmd_analyze
    * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
  0: typecast
      * type: pointer
          * #source_location: 
            * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
            * line: 9112
            * function: cmd_analyze
            * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
          * width: 32
          0: signedbv
              * width: 8
              * #constant: 1
              * #c_type: char
      * #source_location: 
        * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
        * line: 9112
        * function: cmd_analyze
        * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
      * #lvalue: 1
      0: symbol
          * type: pointer
              * #source_location: 
                * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
                * line: 9074
                * function: cmd_analyze
                * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
              * width: 32
              0: unsignedbv
                  * width: 8
                  * #typedef: uchar
                  * #c_type: unsigned_char
          * #source_location: 
            * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
            * line: 9112
            * function: cmd_analyze
            * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
          * identifier: cmd_analyze::1::temp
          * #lvalue: 1
typecast
  * type: pointer
      * #source_location: 
        * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
        * line: 9112
        * function: cmd_analyze
        * 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/dnspod-sr/main.c
    * line: 9112
    * function: cmd_analyze
    * 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: 6
                  0: signedbv
                      * width: 8
                      * #c_type: char
              * #source_location: 
                * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
                * line: 9112
                * function: cmd_analyze
                * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
              * value: %s %s
              * #lvalue: 1
          1: constant
              * type: signedbv
                  * width: 32
                  * #c_type: signed_int
              * value: 0
symbol
  * type: pointer
      * #source_location: 
        * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
        * line: 9070
        * function: cmd_analyze
        * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
      * width: 32
      0: unsignedbv
          * width: 8
          * #typedef: uchar
          * #c_type: unsigned_char
  * #source_location: 
    * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
    * line: 9113
    * function: cmd_analyze
    * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
  * identifier: cmd_analyze::domain
  * #lvalue: 1
typecast
  * type: pointer
      * width: 32
      0: empty
          * #constant: 1
  0: address_of
      * type: pointer
          * width: 32
          0: unsignedbv
              * width: 8
              * #typedef: uchar
              * #c_type: unsigned_char
      0: index
          * type: unsignedbv
              * width: 8
              * #typedef: uchar
              * #c_type: unsigned_char
          0: symbol
              * type: array
                  * #source_location: 
                    * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
                    * line: 9075
                    * function: cmd_analyze
                    * 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/dnspod-sr/main.c
                        * line: 9075
                        * function: cmd_analyze
                        * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
                      * value: 20
                      * #base: 10
                  0: unsignedbv
                      * width: 8
                      * #typedef: uchar
                      * #c_type: unsigned_char
              * #source_location: 
                * file: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c
                * line: 9113
                * function: cmd_analyze
                * working_directory: /mnt/goblint-svcomp/benchexec/tools-pldi24/deagle
              * identifier: cmd_analyze::1::str_type
              * #lvalue: 1
          1: constant
              * type: signedbv
                  * width: 32
                  * #c_type: signed_int
              * value: 0
Adding CPROVER library (x86_64)
file <builtin-library-time> line 11: warning: conflicting return types "time"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 8341
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/dnspod-sr/main.c line 8341
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-fopen> line 15: warning: conflicting return types "fopen"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 5859
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/dnspod-sr/main.c line 5859
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-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/dnspod-sr/main.c line 5858
signed int (FILE *)
new definition in module <built-in-library> file <builtin-library-fclose> line 14
signed int (FILE *stream)
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/dnspod-sr/main.c line 5864
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-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/dnspod-sr/main.c line 5860
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-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/dnspod-sr/main.c line 808
signed int (FILE *)
new definition in module <built-in-library> file <builtin-library-fflush> line 9
signed int (FILE *stream)
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/dnspod-sr/main.c line 2668
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 /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/dnspod-sr/main.c line 807
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/dnspod-sr/main.c line 5857
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;
} *
Removal of function pointers and virtual functions
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 1925 function insert_node: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 1936 function insert_node: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 1887 function find_node: replacing function pointer by 3 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 3531 function htable_insert: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 3543 function htable_insert: replacing function pointer by 1 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 3256 function htable_delete: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 3273 function htable_delete: replacing function pointer by 1 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 3026 function htable_find: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 3037 function htable_find: replacing function pointer by 1 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 3170 function htable_find_list: replacing function pointer by 1 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 3398 function htable_delete_list: replacing function pointer by 1 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 3605 function htable_insert_list: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 3617 function htable_insert_list: replacing function pointer by 1 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c line 6999 function run_sentinel: replacing function pointer by 3 possible targets
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 6 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
too many unwind!
