./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i


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


Deagle version 2.1 64-bit x86_64 linux
which contains:
CBMC version 5.67.0 (SVCOMP2023_221122-2-g2121ef1a2) 64-bit x86_64 linux
Parsing /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i
Converting
Type-checking race-3_1-container_of-global
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module race-3_1-container_of-global file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i line 392
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_init> line 27: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_init"
old definition in module race-3_1-container_of-global file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i line 498
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-pthread_mutex_lock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_lock"
old definition in module race-3_1-container_of-global file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i line 505
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_unlock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_unlock"
old definition in module race-3_1-container_of-global file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i line 510
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_destroy> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_destroy"
old definition in module race-3_1-container_of-global file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i line 501
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)
Removal of function pointers and virtual functions
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 1 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
[Warning][Unknown] Unknown value in {&data} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1750:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1722:2)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1711:2)
[Debug][Unknown] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
[Debug][Analyzer] Base EvalInt data->shared.b query answering bot instead of Unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
[Debug][Analyzer] Base EvalInt data->shared.b + 1 query answering bot instead of Unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1711:2)
[Debug][Unknown] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
[Debug][Analyzer] Base EvalInt data->shared.b query answering bot instead of Unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
[Debug][Analyzer] Base EvalInt data->shared.b + 1 query answering bot instead of Unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
[Warning][Unknown] Unknown value in {&data} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1752:4)
[Debug][Analyzer] Base EvalInt t1 query answering bot instead of {([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1727:2, main], {})} (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1735:2)
[Warning][Unknown] Unknown address in {&status} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1735:2)
[Debug][Analyzer] Base EvalInt t2 query answering bot instead of {([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1728:2, main], {})} (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1736:2)
[Warning][Unknown] Unknown value in {&data.lock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1737:2)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:55:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:60:1)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:65:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:70:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:75:1)
[Warning][Race] Memory location (struct my_data).shared.b (race with conf. 100):
  read with {thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1727:2, main], {})} (conf. 100) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
  read with {thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1728:2, main], {})} (conf. 100) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
  write with {thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1727:2, main], {})} (conf. 100) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
  write with {thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1728:2, main], {})} (conf. 100) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1712:2)
[Warning][Race] Memory location (struct my_data).shared.a (race with conf. 100):
  write with {thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1727:2, main], {})} (conf. 100) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1711:2)
  write with {thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1728:2, main], {})} (conf. 100) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i:1711:2)

Summary for all memory locations:
	safe:            3
	vulnerable:      0
	unsafe:          2
	-------------------
	total:           5
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
Handling datarace, passing the problem to goblint first
getcwd: /mnt/goblint-svcomp/benchexec/tools-pldi/deagle
/mnt/goblint-svcomp/benchexec/tools-pldi/deagle/goblint/goblint /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 1711 1712 1713 1722 1723 1735 1736 1737 
The number of races before goblint filter: 1088
The number of races after goblint filter: 312
Race categories: 8
	1711(1) - 1711(1) main::1::1::data!0@1:
		main::1::1::data!0@1#10..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#16..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#16..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#11..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#17..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#17..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#12..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#18..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#18..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#30..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#31..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#32..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#34..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#35..lock
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#36..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#37..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#38..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#40..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#41..shared..a
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#36..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#37..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#38..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#40..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#41..shared..b
		main::1::1::data!0@1#14..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#20..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#20..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#15..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#21..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#21..shared..b main::1::1::data!0@1#39..shared..b
	1711(1) - 1712(1) main::1::1::data!0@1:
		main::1::1::data!0@1#10..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#16..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#16..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#11..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#17..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#17..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#12..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#18..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#18..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#36..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#37..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#38..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#39..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#41..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#42..lock
		main::1::1::data!0@1#13..lock main::1::1::data!0@1#43..lock
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#42..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#43..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#44..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#45..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#47..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#48..shared..a
		main::1::1::data!0@1#19..shared..a main::1::1::data!0@1#49..shared..a
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#42..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#43..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#44..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#45..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#47..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#48..shared..b
		main::1::1::data!0@1#19..shared..b main::1::1::data!0@1#49..shared..b
		main::1::1::data!0@1#14..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#20..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#20..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#15..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#21..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#21..shared..b main::1::1::data!0@1#46..shared..b
	1712(1) - 1711(1) main::1::1::data!0@1:
		main::1::1::data!0@1#16..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#22..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#22..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#17..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#23..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#23..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#18..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#24..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#24..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#19..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#25..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#25..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#30..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#31..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#32..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#34..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#35..lock
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#36..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#37..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#38..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#40..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#41..shared..a
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#36..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#37..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#38..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#40..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#41..shared..b
		main::1::1::data!0@1#21..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#27..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#27..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#22..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#28..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#28..shared..b main::1::1::data!0@1#39..shared..b
		main::1::1::data!0@1#23..lock main::1::1::data!0@1#33..lock
		main::1::1::data!0@1#29..shared..a main::1::1::data!0@1#39..shared..a
		main::1::1::data!0@1#29..shared..b main::1::1::data!0@1#39..shared..b
	1712(1) - 1712(1) main::1::1::data!0@1:
		main::1::1::data!0@1#16..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#22..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#22..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#17..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#23..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#23..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#18..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#24..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#24..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#19..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#25..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#25..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#36..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#37..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#38..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#39..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#41..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#42..lock
		main::1::1::data!0@1#20..lock main::1::1::data!0@1#43..lock
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#42..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#43..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#44..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#45..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#47..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#48..shared..a
		main::1::1::data!0@1#26..shared..a main::1::1::data!0@1#49..shared..a
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#42..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#43..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#44..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#45..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#47..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#48..shared..b
		main::1::1::data!0@1#26..shared..b main::1::1::data!0@1#49..shared..b
		main::1::1::data!0@1#21..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#27..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#27..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#22..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#28..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#28..shared..b main::1::1::data!0@1#46..shared..b
		main::1::1::data!0@1#23..lock main::1::1::data!0@1#40..lock
		main::1::1::data!0@1#29..shared..a main::1::1::data!0@1#46..shared..a
		main::1::1::data!0@1#29..shared..b main::1::1::data!0@1#46..shared..b
	1711(1) - 1711(1) my_callback::1::data$object:
		my_callback::1::data$object#1..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#1..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#1..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#2..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#2..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#2..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#3..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#3..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#3..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#4..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#4..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#4..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#5..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#5..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#5..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#6..lock my_callback::1::data$object#15..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#16..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#17..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#18..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#19..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#15..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#16..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#17..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#18..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#19..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#15..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#16..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#17..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#18..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#19..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#20..shared..b
	1711(1) - 1712(1) my_callback::1::data$object:
		my_callback::1::data$object#1..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#1..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#1..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#2..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#2..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#2..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#3..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#3..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#3..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#4..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#4..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#4..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#5..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#5..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#5..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#6..lock my_callback::1::data$object#21..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#22..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#23..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#24..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#25..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#26..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#27..lock
		my_callback::1::data$object#6..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#21..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#22..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#23..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#24..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#25..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#26..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#27..shared..a
		my_callback::1::data$object#6..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#21..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#22..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#23..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#24..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#25..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#26..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#27..shared..b
		my_callback::1::data$object#6..shared..b my_callback::1::data$object#28..shared..b
	1712(1) - 1711(1) my_callback::1::data$object:
		my_callback::1::data$object#7..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#7..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#7..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#8..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#8..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#8..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#9..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#9..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#9..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#10..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#10..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#10..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#11..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#11..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#11..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#12..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#12..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#12..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#13..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#13..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#13..shared..b my_callback::1::data$object#20..shared..b
		my_callback::1::data$object#14..lock my_callback::1::data$object#15..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#16..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#17..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#18..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#19..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#20..lock
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#15..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#16..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#17..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#18..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#19..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#20..shared..a
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#15..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#16..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#17..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#18..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#19..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#20..shared..b
	1712(1) - 1712(1) my_callback::1::data$object:
		my_callback::1::data$object#7..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#7..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#7..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#8..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#8..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#8..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#9..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#9..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#9..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#10..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#10..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#10..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#11..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#11..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#11..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#12..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#12..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#12..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#13..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#13..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#13..shared..b my_callback::1::data$object#28..shared..b
		my_callback::1::data$object#14..lock my_callback::1::data$object#21..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#22..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#23..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#24..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#25..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#26..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#27..lock
		my_callback::1::data$object#14..lock my_callback::1::data$object#28..lock
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#21..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#22..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#23..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#24..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#25..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#26..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#27..shared..a
		my_callback::1::data$object#14..shared..a my_callback::1::data$object#28..shared..a
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#21..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#22..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#23..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#24..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#25..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#26..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#27..shared..b
		my_callback::1::data$object#14..shared..b my_callback::1::data$object#28..shared..b
Runtime Symex: 2.14774s
Adding SC constraints
Shared __CPROVER_threads_exited: 4R/3W
Shared __CPROVER_next_thread_id: 3R/3W
Shared t1: 2R/2W
Shared t2: 2R/2W
Shared my_dev: 2R/2W
Shared main::1::1::data!0@1..lock: 30R/11W
Shared main::1::1::data!0@1..shared..a: 34R/13W
Shared main::1::1::data!0@1..shared..b: 34R/13W
Shared my_callback::1::data$object..lock: 24R/5W
Shared my_callback::1::data$object..shared..a: 24R/5W
Shared my_callback::1::data$object..shared..b: 24R/5W
size of program expression: 2453 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0598797s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0737751s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.000930007s
Solving with Deagle's Closure solver
111846 variables, 461543 clauses
ClosureSolver finishes with 84 conflicts, 54492 decisions, and 308268 propagations. 1004 theory propagations and 3 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0621916s
Runtime decision procedure: 0.170494s
Running propositional reduction
Solving with Deagle's Closure solver
111846 variables, 459917 clauses
ClosureSolver finishes with 463 conflicts, 634662 decisions, and 4839649 propagations. 12718 theory propagations and 6 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.904536s
Runtime decision procedure: 0.904575s
Running propositional reduction
Solving with Deagle's Closure solver
111846 variables, 439227 clauses
ClosureSolver finishes with 463 conflicts, 650050 decisions, and 4948681 propagations. 13012 theory propagations and 6 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0245052s
Runtime decision procedure: 0.0245425s
Running propositional reduction
Solving with Deagle's Closure solver
111846 variables, 439227 clauses
ClosureSolver finishes with 466 conflicts, 665833 decisions, and 5063353 propagations. 13631 theory propagations and 8 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0326839s
Runtime decision procedure: 0.0327208s
Running propositional reduction
Solving with Deagle's Closure solver
111846 variables, 439195 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 5.37e-06s
Runtime decision procedure: 1.8761e-05s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_1-container_of-global.i function my_drv_probe
[nodatarace.assertion.0] line 1728 No data races on variable main::1::1::data!0@1 between line 1711 and line 1711: FAILURE
[nodatarace.assertion.1] line 1728 No data races on variable main::1::1::data!0@1 between line 1711 and line 1712: FAILURE
[nodatarace.assertion.2] line 1728 No data races on variable main::1::1::data!0@1 between line 1712 and line 1711: FAILURE
[nodatarace.assertion.3] line 1728 No data races on variable main::1::1::data!0@1 between line 1712 and line 1712: FAILURE
[nodatarace.assertion.4] line 1728 No data races on variable my_callback::1::data$object between line 1711 and line 1711: SUCCESS
[nodatarace.assertion.5] line 1728 No data races on variable my_callback::1::data$object between line 1711 and line 1712: SUCCESS
[nodatarace.assertion.6] line 1728 No data races on variable my_callback::1::data$object between line 1712 and line 1711: SUCCESS
[nodatarace.assertion.7] line 1728 No data races on variable my_callback::1::data$object between line 1712 and line 1712: SUCCESS

** 4 of 8 failed (5 iterations)
VERIFICATION FAILED
