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


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


./deagle_exe --svcomp --graphml-witness error-witness.graphml --no-assertions --datarace /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/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/lmdb/main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
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/lmdb/main.c line 576
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/lmdb/main.c line 575
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/lmdb/main.c line 574
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/lmdb/main.c line 572
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-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/lmdb/main.c line 524
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/lmdb/main.c line 10602
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/lmdb/main.c line 10602
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-mmap> line 23: 
reason for conflict at #this: conflict on POD

__off_t
off_t
error: conflicting function declarations 'mmap'
old definition in module 'main' file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 514
void * (void *, size_t, signed int, signed int, signed int, __off_t)
new definition in module '<built-in-library>' file <builtin-library-mmap> line 23
void * (void *addr, __CPROVER_size_t length, signed int prot, signed int flags, signed int fd, off_t offset)
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/lmdb/main.c line 523
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/lmdb/main.c line 5556 function mdb_cursor_get: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 5737 function mdb_cursor_put: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 5867 function mdb_cursor_put: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 780 function mdb_cmp: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 796 function mdb_dcmp: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 4268 function mdb_node_search: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 4284 function mdb_node_search: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 5057 function mdb_cursor_set: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 5075 function mdb_cursor_set: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 5092 function mdb_cursor_set: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 5216 function mdb_cursor_set: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 1190 function mdb_page_dirty: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 9956 function mdb_reader_list: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 9974 function mdb_reader_list: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 9979 function mdb_reader_list: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 9987 function mdb_reader_list: replacing function pointer by 7 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 769 function mdb_assert_fail: replacing function pointer by 7 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 main.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 10664 function main thread 0
Not unwinding loop main.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c line 10664 function main thread 0
Start removing dummy accesses: 171 steps before removal
171 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: 0.0063255s
size of program expression: 171 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 9.92e-06s

** Results:
/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_cursor_del
[mdb_cursor_del.precondition_instance.1] line 6312 memcpy src/dst overlap: SUCCESS
[mdb_cursor_del.precondition_instance.2] line 6312 memcpy source region readable: SUCCESS
[mdb_cursor_del.precondition_instance.3] line 6312 memcpy destination region writeable: SUCCESS
[mdb_cursor_del.precondition_instance.4] line 6372 memcpy src/dst overlap: SUCCESS
[mdb_cursor_del.precondition_instance.5] line 6372 memcpy source region readable: SUCCESS
[mdb_cursor_del.precondition_instance.6] line 6372 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_cursor_put
[mdb_cursor_put.precondition_instance.1] line 5816 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.2] line 5816 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.3] line 5816 memcpy destination region writeable: SUCCESS
[mdb_cursor_put.precondition_instance.4] line 5875 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.5] line 5875 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.6] line 5875 memcpy destination region writeable: SUCCESS
[mdb_cursor_put.precondition_instance.7] line 5952 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.8] line 5952 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.9] line 5952 memcpy destination region writeable: SUCCESS
[mdb_cursor_put.precondition_instance.10] line 5956 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.11] line 5956 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.12] line 5956 memcpy destination region writeable: SUCCESS
[mdb_cursor_put.precondition_instance.13] line 5959 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.14] line 5959 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.15] line 5959 memcpy destination region writeable: SUCCESS
[mdb_cursor_put.precondition_instance.16] line 5982 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.17] line 5982 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.18] line 5982 memcpy destination region writeable: SUCCESS
[mdb_cursor_put.precondition_instance.19] line 6020 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.20] line 6020 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.21] line 6020 memcpy destination region writeable: SUCCESS
[mdb_cursor_put.precondition_instance.22] line 6024 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.23] line 6024 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.24] line 6024 memcpy destination region writeable: SUCCESS
[mdb_cursor_put.precondition_instance.25] line 6036 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.26] line 6036 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.27] line 6036 memcpy destination region writeable: SUCCESS
[mdb_cursor_put.precondition_instance.28] line 6052 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.29] line 6052 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.30] line 6052 memcpy destination region writeable: SUCCESS
[mdb_cursor_put.precondition_instance.31] line 6055 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.32] line 6055 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.33] line 6055 memcpy destination region writeable: SUCCESS
[mdb_cursor_put.precondition_instance.34] line 6214 memcpy src/dst overlap: SUCCESS
[mdb_cursor_put.precondition_instance.35] line 6214 memcpy source region readable: SUCCESS
[mdb_cursor_put.precondition_instance.36] line 6214 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_dbi_open
[mdb_dbi_open.precondition_instance.1] line 9529 memset destination region writeable: SUCCESS
[mdb_dbi_open.precondition_instance.2] line 9565 memcpy src/dst overlap: SUCCESS
[mdb_dbi_open.precondition_instance.3] line 9565 memcpy source region readable: SUCCESS
[mdb_dbi_open.precondition_instance.4] line 9565 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_drop0
[mdb_drop0.precondition_instance.1] line 9686 memcpy src/dst overlap: SUCCESS
[mdb_drop0.precondition_instance.2] line 9686 memcpy source region readable: SUCCESS
[mdb_drop0.precondition_instance.3] line 9686 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_env_copyfd1
[mdb_env_copyfd1.precondition_instance.1] line 8957 memset destination region writeable: SUCCESS
[mdb_env_copyfd1.precondition_instance.2] line 8972 memset destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_env_cwalk
[mdb_env_cwalk.precondition_instance.1] line 8783 memcpy src/dst overlap: SUCCESS
[mdb_env_cwalk.precondition_instance.2] line 8783 memcpy source region readable: SUCCESS
[mdb_env_cwalk.precondition_instance.3] line 8783 memcpy destination region writeable: SUCCESS
[mdb_env_cwalk.precondition_instance.4] line 8785 memcpy src/dst overlap: SUCCESS
[mdb_env_cwalk.precondition_instance.5] line 8785 memcpy source region readable: SUCCESS
[mdb_env_cwalk.precondition_instance.6] line 8785 memcpy destination region writeable: SUCCESS
[mdb_env_cwalk.precondition_instance.7] line 8799 memcpy src/dst overlap: SUCCESS
[mdb_env_cwalk.precondition_instance.8] line 8799 memcpy source region readable: SUCCESS
[mdb_env_cwalk.precondition_instance.9] line 8799 memcpy destination region writeable: SUCCESS
[mdb_env_cwalk.precondition_instance.10] line 8820 memcpy src/dst overlap: SUCCESS
[mdb_env_cwalk.precondition_instance.11] line 8820 memcpy source region readable: SUCCESS
[mdb_env_cwalk.precondition_instance.12] line 8820 memcpy destination region writeable: SUCCESS
[mdb_env_cwalk.precondition_instance.13] line 8828 memcpy src/dst overlap: SUCCESS
[mdb_env_cwalk.precondition_instance.14] line 8828 memcpy source region readable: SUCCESS
[mdb_env_cwalk.precondition_instance.15] line 8828 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_env_excl_lock
[mdb_env_excl_lock.precondition_instance.1] line 3705 memset destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_env_open2
[mdb_env_open2.precondition_instance.1] line 3595 memset destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_env_setup_locks
[mdb_env_setup_locks.precondition_instance.1] line 3808 memset destination region writeable: SUCCESS
[mdb_env_setup_locks.precondition_instance.2] line 3809 memset destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_env_share_locks
[mdb_env_share_locks.precondition_instance.1] line 3670 memset destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_freelist_save
[mdb_freelist_save.precondition_instance.1] line 2463 memcpy src/dst overlap: SUCCESS
[mdb_freelist_save.precondition_instance.2] line 2463 memcpy source region readable: SUCCESS
[mdb_freelist_save.precondition_instance.3] line 2463 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_midl_append_list
[mdb_midl_append_list.precondition_instance.1] line 10342 memcpy src/dst overlap: SUCCESS
[mdb_midl_append_list.precondition_instance.2] line 10342 memcpy source region readable: SUCCESS
[mdb_midl_append_list.precondition_instance.3] line 10342 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_midl_grow
[mdb_midl_grow.precondition_instance.1] line 10273 realloc argument is dynamic object: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_midl_need
[mdb_midl_need.precondition_instance.1] line 10296 realloc argument is dynamic object: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_midl_shrink
[mdb_midl_shrink.precondition_instance.1] line 10253 realloc argument is dynamic object: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_node_add
[mdb_node_add.precondition_instance.1] line 6476 memmove source region readable: SUCCESS
[mdb_node_add.precondition_instance.2] line 6476 memmove destination region writeable: SUCCESS
[mdb_node_add.precondition_instance.3] line 6478 memcpy src/dst overlap: SUCCESS
[mdb_node_add.precondition_instance.4] line 6478 memcpy source region readable: SUCCESS
[mdb_node_add.precondition_instance.5] line 6478 memcpy destination region writeable: SUCCESS
[mdb_node_add.precondition_instance.6] line 6556 memcpy src/dst overlap: SUCCESS
[mdb_node_add.precondition_instance.7] line 6556 memcpy source region readable: SUCCESS
[mdb_node_add.precondition_instance.8] line 6556 memcpy destination region writeable: SUCCESS
[mdb_node_add.precondition_instance.9] line 6563 memcpy src/dst overlap: SUCCESS
[mdb_node_add.precondition_instance.10] line 6563 memcpy source region readable: SUCCESS
[mdb_node_add.precondition_instance.11] line 6563 memcpy destination region writeable: SUCCESS
[mdb_node_add.precondition_instance.12] line 6569 memcpy src/dst overlap: SUCCESS
[mdb_node_add.precondition_instance.13] line 6569 memcpy source region readable: SUCCESS
[mdb_node_add.precondition_instance.14] line 6569 memcpy destination region writeable: SUCCESS
[mdb_node_add.precondition_instance.15] line 6573 memcpy src/dst overlap: SUCCESS
[mdb_node_add.precondition_instance.16] line 6573 memcpy source region readable: SUCCESS
[mdb_node_add.precondition_instance.17] line 6573 memcpy destination region writeable: SUCCESS
[mdb_node_add.precondition_instance.18] line 6579 memcpy src/dst overlap: SUCCESS
[mdb_node_add.precondition_instance.19] line 6579 memcpy source region readable: SUCCESS
[mdb_node_add.precondition_instance.20] line 6579 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_node_del
[mdb_node_del.precondition_instance.1] line 6615 memmove source region readable: SUCCESS
[mdb_node_del.precondition_instance.2] line 6615 memmove destination region writeable: SUCCESS
[mdb_node_del.precondition_instance.3] line 6645 memmove source region readable: SUCCESS
[mdb_node_del.precondition_instance.4] line 6645 memmove destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_node_read
[mdb_node_read.precondition_instance.1] line 4740 memcpy src/dst overlap: SUCCESS
[mdb_node_read.precondition_instance.2] line 4740 memcpy source region readable: SUCCESS
[mdb_node_read.precondition_instance.3] line 4740 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_node_shrink
[mdb_node_shrink.precondition_instance.1] line 6693 memmove source region readable: SUCCESS
[mdb_node_shrink.precondition_instance.2] line 6693 memmove destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_page_copy
[mdb_page_copy.precondition_instance.1] line 1388 memcpy src/dst overlap: SUCCESS
[mdb_page_copy.precondition_instance.2] line 1388 memcpy source region readable: SUCCESS
[mdb_page_copy.precondition_instance.3] line 1388 memcpy destination region writeable: SUCCESS
[mdb_page_copy.precondition_instance.4] line 1389 memcpy src/dst overlap: SUCCESS
[mdb_page_copy.precondition_instance.5] line 1389 memcpy source region readable: SUCCESS
[mdb_page_copy.precondition_instance.6] line 1389 memcpy destination region writeable: SUCCESS
[mdb_page_copy.precondition_instance.7] line 1392 memcpy src/dst overlap: SUCCESS
[mdb_page_copy.precondition_instance.8] line 1392 memcpy source region readable: SUCCESS
[mdb_page_copy.precondition_instance.9] line 1392 memcpy destination region writeable: SUCCESS
[mdb_page_copy.precondition_instance.10] line 1395 memcpy src/dst overlap: SUCCESS
[mdb_page_copy.precondition_instance.11] line 1395 memcpy source region readable: SUCCESS
[mdb_page_copy.precondition_instance.12] line 1395 memcpy destination region writeable: SUCCESS
[mdb_page_malloc.precondition_instance.1] memset destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_page_search
[mdb_page_search.precondition_instance.1] line 4558 memcpy src/dst overlap: SUCCESS
[mdb_page_search.precondition_instance.2] line 4558 memcpy source region readable: SUCCESS
[mdb_page_search.precondition_instance.3] line 4558 memcpy destination region writeable: SUCCESS
[mdb_page_search.precondition_instance.4] line 4563 memcpy src/dst overlap: SUCCESS
[mdb_page_search.precondition_instance.5] line 4563 memcpy source region readable: SUCCESS
[mdb_page_search.precondition_instance.6] line 4563 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_page_split
[mdb_page_split.precondition_instance.1] line 8114 memcpy src/dst overlap: SUCCESS
[mdb_page_split.precondition_instance.2] line 8114 memcpy source region readable: SUCCESS
[mdb_page_split.precondition_instance.3] line 8114 memcpy destination region writeable: SUCCESS
[mdb_page_split.precondition_instance.4] line 8117 memmove source region readable: SUCCESS
[mdb_page_split.precondition_instance.5] line 8117 memmove destination region writeable: SUCCESS
[mdb_page_split.precondition_instance.6] line 8118 memcpy src/dst overlap: SUCCESS
[mdb_page_split.precondition_instance.7] line 8118 memcpy source region readable: SUCCESS
[mdb_page_split.precondition_instance.8] line 8118 memcpy destination region writeable: SUCCESS
[mdb_page_split.precondition_instance.9] line 8124 memcpy src/dst overlap: SUCCESS
[mdb_page_split.precondition_instance.10] line 8124 memcpy source region readable: SUCCESS
[mdb_page_split.precondition_instance.11] line 8124 memcpy destination region writeable: SUCCESS
[mdb_page_split.precondition_instance.12] line 8128 memcpy src/dst overlap: SUCCESS
[mdb_page_split.precondition_instance.13] line 8128 memcpy source region readable: SUCCESS
[mdb_page_split.precondition_instance.14] line 8128 memcpy destination region writeable: SUCCESS
[mdb_page_split.precondition_instance.15] line 8130 memcpy src/dst overlap: SUCCESS
[mdb_page_split.precondition_instance.16] line 8130 memcpy source region readable: SUCCESS
[mdb_page_split.precondition_instance.17] line 8130 memcpy destination region writeable: SUCCESS
[mdb_page_split.precondition_instance.18] line 8358 memcpy src/dst overlap: SUCCESS
[mdb_page_split.precondition_instance.19] line 8358 memcpy source region readable: SUCCESS
[mdb_page_split.precondition_instance.20] line 8358 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_page_unspill
[mdb_page_unspill.precondition_instance.1] line 1438 memcpy src/dst overlap: SUCCESS
[mdb_page_unspill.precondition_instance.2] line 1438 memcpy source region readable: SUCCESS
[mdb_page_unspill.precondition_instance.3] line 1438 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_reader_pid
[mdb_reader_pid.precondition_instance.1] line 1802 memset destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_txn_begin
[mdb_txn_begin.precondition_instance.1] line 2084 memcpy src/dst overlap: SUCCESS
[mdb_txn_begin.precondition_instance.2] line 2084 memcpy source region readable: SUCCESS
[mdb_txn_begin.precondition_instance.3] line 2084 memcpy destination region writeable: SUCCESS
[mdb_txn_begin.precondition_instance.4] line 2098 memcpy src/dst overlap: SUCCESS
[mdb_txn_begin.precondition_instance.5] line 2098 memcpy source region readable: SUCCESS
[mdb_txn_begin.precondition_instance.6] line 2098 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_txn_commit
[mdb_txn_commit.precondition_instance.1] line 2804 memcpy src/dst overlap: SUCCESS
[mdb_txn_commit.precondition_instance.2] line 2804 memcpy source region readable: SUCCESS
[mdb_txn_commit.precondition_instance.3] line 2804 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_txn_renew0
[mdb_txn_renew0.precondition_instance.1] line 1958 memcpy src/dst overlap: SUCCESS
[mdb_txn_renew0.precondition_instance.2] line 1958 memcpy source region readable: SUCCESS
[mdb_txn_renew0.precondition_instance.3] line 1958 memcpy destination region writeable: SUCCESS
[mdb_txn_renew0.precondition_instance.4] line 1961 memcpy src/dst overlap: SUCCESS
[mdb_txn_renew0.precondition_instance.5] line 1961 memcpy source region readable: SUCCESS
[mdb_txn_renew0.precondition_instance.6] line 1961 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_update_key
[mdb_update_key.precondition_instance.1] line 7047 memmove source region readable: SUCCESS
[mdb_update_key.precondition_instance.2] line 7047 memmove destination region writeable: SUCCESS
[mdb_update_key.precondition_instance.3] line 7055 memcpy src/dst overlap: SUCCESS
[mdb_update_key.precondition_instance.4] line 7055 memcpy source region readable: SUCCESS
[mdb_update_key.precondition_instance.5] line 7055 memcpy destination region writeable: SUCCESS

/mnt/goblint-svcomp/goblint-bench/bench/concrat/lmdb/main.c function mdb_xcursor_init1
[mdb_xcursor_init1.precondition_instance.1] line 6741 memcpy src/dst overlap: SUCCESS
[mdb_xcursor_init1.precondition_instance.2] line 6741 memcpy source region readable: SUCCESS
[mdb_xcursor_init1.precondition_instance.3] line 6741 memcpy destination region writeable: SUCCESS

<builtin-library-memcmp> function memcmp
[memcmp.precondition.1] line 19 memcmp region 1 readable: SUCCESS
[memcmp.precondition.2] line 21 memcpy region 2 readable: SUCCESS

** 0 of 177 failed (1 iterations)
VERIFICATION SUCCESSFUL
