./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.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/pthread-divine/one_time_barrier_2t.i
Converting
Type-checking one_time_barrier_2t
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_cond_init> line 7: 
reason for conflict at #this.__data: names of member 0 differ ($anon0/__wseq)

struct __pthread_cond_s {
  union $anon0;
  union $anon1;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
struct __pthread_cond_s {
  __atomic_wide_counter __wseq;
  __atomic_wide_counter __g1_start;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
warning: pointer parameter types differ between declaration and definition "pthread_cond_init"
old definition in module one_time_barrier_2t file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 609
signed int (pthread_cond_t *, const pthread_condattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_init> line 7
signed int (pthread_cond_t *cond, const pthread_condattr_t *attr)
file <builtin-library-pthread_mutex_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 one_time_barrier_2t file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 518
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_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 one_time_barrier_2t file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 511
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_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 one_time_barrier_2t file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 523
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_cond_broadcast> line 7: 
reason for conflict at #this.__data: names of member 0 differ ($anon0/__wseq)

struct __pthread_cond_s {
  union $anon0;
  union $anon1;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
struct __pthread_cond_s {
  __atomic_wide_counter __wseq;
  __atomic_wide_counter __g1_start;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
warning: pointer parameter types differ between declaration and definition "pthread_cond_broadcast"
old definition in module one_time_barrier_2t file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 616
signed int (pthread_cond_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_broadcast> line 7
signed int (pthread_cond_t *cond)
file <builtin-library-pthread_cond_wait> line 7: 
reason for conflict at #this.__data: names of member 0 differ ($anon0/__wseq)

struct __pthread_cond_s {
  union $anon0;
  union $anon1;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
struct __pthread_cond_s {
  __atomic_wide_counter __wseq;
  __atomic_wide_counter __g1_start;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
warning: pointer parameter types differ between declaration and definition "pthread_cond_wait"
old definition in module one_time_barrier_2t file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 618
signed int (pthread_cond_t *, pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_wait> line 7
signed int (pthread_cond_t *cond, pthread_mutex_t *mutex)
file <builtin-library-pthread_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module one_time_barrier_2t file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 405
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)
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
worker_fn::1::sig's upper bound is 1
worker_fn::1::sig's upper bound is 1
set limit type 1
Use SV-COMP unwinding strategy: 3
Deagle's solver is set!!!!!!
Unwinding loop main.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 772 function main thread 0
Unwinding loop main.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 772 function main thread 0
Unwinding loop main.1 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 779 function main thread 0
Unwinding loop worker_fn.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 739 function worker_fn thread 0
Unwinding loop worker_fn.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 739 function worker_fn thread 0
Unwinding loop barrier_wait.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 0
Unwinding loop barrier_wait.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 0
Not unwinding loop barrier_wait.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 0
Unwinding loop worker_fn.1 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 745 function worker_fn thread 0
Unwinding loop worker_fn.1 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 745 function worker_fn thread 0
Unwinding loop barrier_wait.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 0
Unwinding loop barrier_wait.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 0
Not unwinding loop barrier_wait.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 0
Unwinding loop worker_fn.2 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 756 function worker_fn thread 0
Unwinding loop worker_fn.2 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 756 function worker_fn thread 0
Unwinding loop worker_fn.3 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 763 function worker_fn thread 0
Unwinding loop worker_fn.3 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 763 function worker_fn thread 0
Unwinding loop main.2 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 782 function main thread 0
Unwinding loop main.3 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 785 function main thread 0
Unwinding loop main.3 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 785 function main thread 0
Unwinding loop worker_fn.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 739 function worker_fn thread 1
Unwinding loop worker_fn.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 739 function worker_fn thread 1
Unwinding loop barrier_wait.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 1
Unwinding loop barrier_wait.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 1
Not unwind[Warning][Unknown] Unknown value in {&b1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:777:5)
[Warning][Unknown] Unknown value in {&b1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:780:9)
[Warning][Unknown] Unknown value in {&b1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:743:5)
[Warning][Unknown] Unknown value in {&b1.sig} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:719:9)
[Warning][Unknown] Unknown value in {&b1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:752:5)
[Warning][Unknown] Unknown value in {&b1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:781:5)
[Warning][Unknown] Unknown value in {&b1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:743:5)
[Warning][Unknown] Unknown value in {&b1.sig} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:719:9)
[Warning][Unknown] Unknown value in {&b1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:752:5)
[Warning][Deadcode] Function "__bswap_16" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:63:1)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:68:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:73:15)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:78:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:83:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:88:1)
[Warning][Deadcode] Function "barrier_destroy" will never be called: 3LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:710:1)
[Warning][Race] Memory location sig2[?]@one_time_barrier_2t.i:734:26 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:764:9)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:764:9)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:787:9)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:752:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:752:5)
[Warning][Race] Memory location in[?]@one_time_barrier_2t.i:733:26 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:740:10)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:740:10)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:750:6)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:750:6)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:758:10)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:758:10)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:751:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:751:5)
[Warning][Race] Memory location pre[?]@one_time_barrier_2t.i:733:16 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:746:10)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:746:10)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:757:10)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:757:10)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:738:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:738:5)
[Warning][Race] Memory location post[?]@one_time_barrier_2t.i:733:35 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:741:10)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:741:10)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:753:6)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:753:6)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:786:10)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:754:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:754:5)
[Warning][Race] Memory location sig1[?]@one_time_barrier_2t.i:734:15 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:747:9)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:747:9)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:759:9)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:759:9)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:743:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:743:5)
[Warning][Race] Memory location b1.seen@one_time_barrier_2t.i:770:13 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:715:6)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:715:6)
  read with {lock:b1.lock} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:717:5)
  read with {lock:b1.lock, thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:717:5)
  read with {lock:b1.lock} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:718:5)
  read with {lock:b1.lock, thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:718:5)
  read with {lock:b1.lock} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:723:5)
  read with {lock:b1.lock, thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:723:5)
  write with {lock:b1.lock} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:717:5)
  write with {lock:b1.lock, thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i:717:5)

Summary for all memory locations:
	safe:           17
	vulnerable:      0
	unsafe:          6
	-------------------
	total:          23
ing loop barrier_wait.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 1
Unwinding loop worker_fn.1 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 745 function worker_fn thread 1
Unwinding loop worker_fn.1 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 745 function worker_fn thread 1
Unwinding loop barrier_wait.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 1
Unwinding loop barrier_wait.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 1
Not unwinding loop barrier_wait.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 723 function barrier_wait thread 1
Unwinding loop worker_fn.2 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 756 function worker_fn thread 1
Unwinding loop worker_fn.2 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 756 function worker_fn thread 1
Unwinding loop worker_fn.3 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 763 function worker_fn thread 1
Unwinding loop worker_fn.3 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_2t.i line 763 function worker_fn thread 1
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/pthread-divine/one_time_barrier_2t.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 715 716 717 718 719 723 724 738 739 740 741 742 743 744 746 747 748 750 751 752 753 754 755 757 758 759 760 764 765 786 787 788 
The number of races before goblint filter: 1303
The number of races after goblint filter: 162
Race categories: 34
	740(1) - 751(1) in:
		in#2[[0]] in#13[[0]]
		in#2[[1]] in#13[[1]]
		in#3[[0]] in#13[[0]]
		in#3[[1]] in#13[[1]]
	750(1) - 751(1) in:
		in#4[[0]] in#13[[0]]
		in#4[[1]] in#13[[1]]
	751(1) - 740(1) in:
		in#6[[0]] in#9[[0]]
		in#6[[0]] in#10[[0]]
		in#6[[1]] in#9[[1]]
		in#6[[1]] in#10[[1]]
	751(1) - 750(1) in:
		in#6[[0]] in#11[[0]]
		in#6[[1]] in#11[[1]]
	751(1) - 751(1) in:
		in#5[[0]] in#13[[0]]
		in#5[[1]] in#13[[1]]
		in#6[[0]] in#12[[0]]
		in#6[[0]] in#13[[0]]
		in#6[[1]] in#12[[1]]
		in#6[[1]] in#13[[1]]
	751(1) - 758(1) in:
		in#6[[0]] in#14[[0]]
		in#6[[0]] in#15[[0]]
		in#6[[1]] in#14[[1]]
		in#6[[1]] in#15[[1]]
	758(1) - 751(1) in:
		in#7[[0]] in#13[[0]]
		in#7[[1]] in#13[[1]]
		in#8[[0]] in#13[[0]]
		in#8[[1]] in#13[[1]]
	715(1) - 717(1) main::1::b1!0@1:
		main::1::b1!0@1#5..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#5..seen main::1::b1!0@1#100..seen
		main::1::b1!0@1#36..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#36..seen main::1::b1!0@1#100..seen
	717(1) - 715(1) main::1::b1!0@1:
		main::1::b1!0@1#10..seen main::1::b1!0@1#67..seen
		main::1::b1!0@1#10..seen main::1::b1!0@1#95..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#67..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#95..seen
	717(1) - 717(1) main::1::b1!0@1:
		main::1::b1!0@1#9..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#9..seen main::1::b1!0@1#100..seen
		main::1::b1!0@1#10..seen main::1::b1!0@1#71..seen
		main::1::b1!0@1#10..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#10..seen main::1::b1!0@1#99..seen
		main::1::b1!0@1#10..seen main::1::b1!0@1#100..seen
		main::1::b1!0@1#40..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#40..seen main::1::b1!0@1#100..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#71..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#99..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#100..seen
	717(1) - 718(1) main::1::b1!0@1:
		main::1::b1!0@1#10..seen main::1::b1!0@1#73..seen
		main::1::b1!0@1#10..seen main::1::b1!0@1#101..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#73..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#101..seen
	717(1) - 723(1) main::1::b1!0@1:
		main::1::b1!0@1#10..seen main::1::b1!0@1#80..seen
		main::1::b1!0@1#10..seen main::1::b1!0@1#84..seen
		main::1::b1!0@1#10..seen main::1::b1!0@1#88..seen
		main::1::b1!0@1#10..seen main::1::b1!0@1#108..seen
		main::1::b1!0@1#10..seen main::1::b1!0@1#112..seen
		main::1::b1!0@1#10..seen main::1::b1!0@1#116..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#80..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#84..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#88..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#108..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#112..seen
		main::1::b1!0@1#41..seen main::1::b1!0@1#116..seen
	718(1) - 717(1) main::1::b1!0@1:
		main::1::b1!0@1#11..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#11..seen main::1::b1!0@1#100..seen
		main::1::b1!0@1#42..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#42..seen main::1::b1!0@1#100..seen
	723(1) - 717(1) main::1::b1!0@1:
		main::1::b1!0@1#18..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#18..seen main::1::b1!0@1#100..seen
		main::1::b1!0@1#23..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#23..seen main::1::b1!0@1#100..seen
		main::1::b1!0@1#28..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#28..seen main::1::b1!0@1#100..seen
		main::1::b1!0@1#49..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#49..seen main::1::b1!0@1#100..seen
		main::1::b1!0@1#54..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#54..seen main::1::b1!0@1#100..seen
		main::1::b1!0@1#59..seen main::1::b1!0@1#72..seen
		main::1::b1!0@1#59..seen main::1::b1!0@1#100..seen
	741(1) - 754(1) post:
		post#2[[0]] post#13[[0]]
		post#2[[1]] post#13[[1]]
		post#3[[0]] post#13[[0]]
		post#3[[1]] post#13[[1]]
	753(1) - 754(1) post:
		post#4[[0]] post#13[[0]]
		post#4[[1]] post#13[[1]]
	754(1) - 741(1) post:
		post#6[[0]] post#9[[0]]
		post#6[[0]] post#10[[0]]
		post#6[[1]] post#9[[1]]
		post#6[[1]] post#10[[1]]
	754(1) - 753(1) post:
		post#6[[0]] post#11[[0]]
		post#6[[1]] post#11[[1]]
	754(1) - 754(1) post:
		post#5[[0]] post#13[[0]]
		post#5[[1]] post#13[[1]]
		post#6[[0]] post#12[[0]]
		post#6[[0]] post#13[[0]]
		post#6[[1]] post#12[[1]]
		post#6[[1]] post#13[[1]]
	786(1) - 754(1) post:
		post#7[[0]] post#13[[0]]
		post#7[[1]] post#13[[1]]
		post#8[[0]] post#13[[0]]
		post#8[[1]] post#13[[1]]
	738(1) - 738(1) pre:
		pre#2[[0]] pre#9[[0]]
		pre#2[[1]] pre#9[[1]]
		pre#3[[0]] pre#8[[0]]
		pre#3[[0]] pre#9[[0]]
		pre#3[[1]] pre#8[[1]]
		pre#3[[1]] pre#9[[1]]
	738(1) - 746(1) pre:
		pre#3[[0]] pre#10[[0]]
		pre#3[[0]] pre#11[[0]]
		pre#3[[1]] pre#10[[1]]
		pre#3[[1]] pre#11[[1]]
	738(1) - 757(1) pre:
		pre#3[[0]] pre#12[[0]]
		pre#3[[0]] pre#13[[0]]
		pre#3[[1]] pre#12[[1]]
		pre#3[[1]] pre#13[[1]]
	746(1) - 738(1) pre:
		pre#4[[0]] pre#9[[0]]
		pre#4[[1]] pre#9[[1]]
		pre#5[[0]] pre#9[[0]]
		pre#5[[1]] pre#9[[1]]
	757(1) - 738(1) pre:
		pre#6[[0]] pre#9[[0]]
		pre#6[[1]] pre#9[[1]]
		pre#7[[0]] pre#9[[0]]
		pre#7[[1]] pre#9[[1]]
	743(1) - 743(1) sig1:
		sig1#2[[0]] sig1#9[[0]]
		sig1#2[[1]] sig1#9[[1]]
		sig1#3[[0]] sig1#8[[0]]
		sig1#3[[0]] sig1#9[[0]]
		sig1#3[[1]] sig1#8[[1]]
		sig1#3[[1]] sig1#9[[1]]
	743(1) - 747(1) sig1:
		sig1#3[[0]] sig1#10[[0]]
		sig1#3[[0]] sig1#11[[0]]
		sig1#3[[1]] sig1#10[[1]]
		sig1#3[[1]] sig1#11[[1]]
	743(1) - 759(1) sig1:
		sig1#3[[0]] sig1#12[[0]]
		sig1#3[[0]] sig1#13[[0]]
		sig1#3[[1]] sig1#12[[1]]
		sig1#3[[1]] sig1#13[[1]]
	747(1) - 743(1) sig1:
		sig1#4[[0]] sig1#9[[0]]
		sig1#4[[1]] sig1#9[[1]]
		sig1#5[[0]] sig1#9[[0]]
		sig1#5[[1]] sig1#9[[1]]
	759(1) - 743(1) sig1:
		sig1#6[[0]] sig1#9[[0]]
		sig1#6[[1]] sig1#9[[1]]
		sig1#7[[0]] sig1#9[[0]]
		sig1#7[[1]] sig1#9[[1]]
	752(1) - 752(1) sig2:
		sig2#2[[0]] sig2#9[[0]]
		sig2#2[[1]] sig2#9[[1]]
		sig2#3[[0]] sig2#8[[0]]
		sig2#3[[0]] sig2#9[[0]]
		sig2#3[[1]] sig2#8[[1]]
		sig2#3[[1]] sig2#9[[1]]
	752(1) - 764(1) sig2:
		sig2#3[[0]] sig2#10[[0]]
		sig2#3[[0]] sig2#11[[0]]
		sig2#3[[1]] sig2#10[[1]]
		sig2#3[[1]] sig2#11[[1]]
	764(1) - 752(1) sig2:
		sig2#4[[0]] sig2#9[[0]]
		sig2#4[[1]] sig2#9[[1]]
		sig2#5[[0]] sig2#9[[0]]
		sig2#5[[1]] sig2#9[[1]]
	787(1) - 752(1) sig2:
		sig2#6[[0]] sig2#9[[0]]
		sig2#6[[1]] sig2#9[[1]]
		sig2#7[[0]] sig2#9[[0]]
		sig2#7[[1]] sig2#9[[1]]
Runtime Symex: 4.79243s
Unsupported library function!
