./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c


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


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/weaver/popl20-commit-2.wvr.c
Converting
Type-checking popl20-commit-2.wvr
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 popl20-commit-2.wvr file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 22
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 4 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
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
Unwinding loop create_fresh_int_array.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 196 function create_fresh_int_array thread 0
Not unwinding loop create_fresh_int_array.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 196 function create_fresh_int_array 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
Unwinding loop create_fresh_int_array.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 196 function create_fresh_int_array thread 0
Not unwinding loop create_fresh_int_array.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 196 function create_fresh_int_array 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
Unwinding loop create_fresh_int_array.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 196 function create_fresh_int_array thread 0
Not unwinding loop create_fresh_int_array.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 196 function create_fresh_int_array 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
Unwinding loop create_fresh_int_array.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 196 function create_fresh_int_array thread 0
Not unwinding loop create_fresh_int_array.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 196 function create_fresh_int_array 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 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Unwinding loop thread1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 52 function thread1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abor[Warning][Unknown] Invalidating expressions: AddrOf(Var(manager_size,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:152:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(manager_front, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:153:3)
[Warning][Unknown] Invalidating expressions: IndexPI(Lval(Var(arr, NoOffset)), Lval(Var(i, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:197:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(client_front,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:157:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(client_size, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:159:3)
[Warning][Unknown] Invalidating expressions: IndexPI(Lval(Var(arr, NoOffset)), Lval(Var(i, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:197:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(node1_front,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:162:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(node1_size, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:164:3)
[Warning][Unknown] Invalidating expressions: IndexPI(Lval(Var(arr, NoOffset)), Lval(Var(i, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:197:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(node2_front,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:167:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(node2_size, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:169:3)
[Warning][Unknown] Invalidating expressions: IndexPI(Lval(Var(arr, NoOffset)), Lval(Var(i, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:197:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(ok,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:172:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(update, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:173:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:55:5)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:61:5)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:67:5)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:73:5)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:79:5)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:85:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:52:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:52:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(safe,
                                     NoOffset)), AddrOf(Var(ok, NoOffset)), AddrOf(Var(update, NoOffset)), AddrOf(Var(node2_back, NoOffset)), AddrOf(Var(node2_front, NoOffset)), AddrOf(Var(node2_size, NoOffset)), AddrOf(Var(node1_back, NoOffset)), AddrOf(Var(node1_front, NoOffset)), AddrOf(Var(node1_size, NoOffset)), AddrOf(Var(manager_back, NoOffset)), AddrOf(Var(manager_front, NoOffset)), AddrOf(Var(manager_size, NoOffset)), AddrOf(Var(client_back, NoOffset)), AddrOf(Var(client_front, NoOffset)), AddrOf(Var(client_size, NoOffset)), AddrOf(Var(node2, NoOffset)), AddrOf(Var(node1, NoOffset)), AddrOf(Var(client, NoOffset)), AddrOf(Var(manager, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:52:3)
[Warning][Unknown] Unknown address in {&node2} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:52:3)
[Warning][Unknown] Unknown address in {&node1} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:52:3)
[Warning][Unknown] Unknown address in {&client} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:52:3)
[Warning][Unknown] Unknown address in {&manager} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:52:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___8, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:52:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:97:5)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:103:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:94:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:94:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(safe,
                                     NoOffset)), AddrOf(Var(ok, NoOffset)), AddrOf(Var(update, NoOffset)), AddrOf(Var(node2_back, NoOffset)), AddrOf(Var(node2_front, NoOffset)), AddrOf(Var(node2_size, NoOffset)), AddrOf(Var(node1_back, NoOffset)), AddrOf(Var(node1_front, NoOffset)), AddrOf(Var(node1_size, NoOffset)), AddrOf(Var(manager_back, NoOffset)), AddrOf(Var(manager_front, NoOffset)), AddrOf(Var(manager_size, NoOffset)), AddrOf(Var(client_back, NoOffset)), AddrOf(Var(client_front, NoOffset)), AddrOf(Var(client_size, NoOffset)), AddrOf(Var(node2, NoOffset)), AddrOf(Var(node1, NoOffset)), AddrOf(Var(client, NoOffset)), AddrOf(Var(manager, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:94:3)
[Warning][Unknown] Unknown address in {&node2} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:94:3)
[Warning][Unknown] Unknown address in {&node1} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:94:3)
[Warning][Unknown] Unknown address in {&client} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:94:3)
[Warning][Unknown] Unknown address in {&manager} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:94:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:94:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:115:5)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:121:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:112:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:112:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(safe,
                                     NoOffset)), AddrOf(Var(ok, NoOffset)), AddrOf(Var(update, NoOffset)), AddrOf(Var(node2_back, NoOffset)), AddrOf(Var(node2_front, NoOffset)), AddrOf(Var(node2_size, NoOffset)), AddrOf(Var(node1_back, NoOffset)), AddrOf(Var(node1_front, NoOffset)), AddrOf(Var(node1_size, NoOffset)), AddrOf(Var(manager_back, NoOffset)), AddrOf(Var(manager_front, NoOffset)), AddrOf(Var(manager_size, NoOffset)), AddrOf(Var(client_back, NoOffset)), AddrOf(Var(client_front, NoOffset)), AddrOf(Var(client_size, NoOffset)), AddrOf(Var(node2, NoOffset)), AddrOf(Var(node1, NoOffset)), AddrOf(Var(client, NoOffset)), AddrOf(Var(manager, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:112:3)
[Warning][Unknown] Unknown address in {&node2} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:112:3)
[Warning][Unknown] Unknown address in {&node1} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:112:3)
[Warning][Unknown] Unknown address in {&client} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:112:3)
[Warning][Unknown] Unknown address in {&manager} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:112:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:112:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:133:5)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:139:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:130:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:130:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(safe,
                                     NoOffset)), AddrOf(Var(ok, NoOffset)), AddrOf(Var(update, NoOffset)), AddrOf(Var(node2_back, NoOffset)), AddrOf(Var(node2_front, NoOffset)), AddrOf(Var(node2_size, NoOffset)), AddrOf(Var(node1_back, NoOffset)), AddrOf(Var(node1_front, NoOffset)), AddrOf(Var(node1_size, NoOffset)), AddrOf(Var(manager_back, NoOffset)), AddrOf(Var(manager_front, NoOffset)), AddrOf(Var(manager_size, NoOffset)), AddrOf(Var(client_back, NoOffset)), AddrOf(Var(client_front, NoOffset)), AddrOf(Var(client_size, NoOffset)), AddrOf(Var(node2, NoOffset)), AddrOf(Var(node1, NoOffset)), AddrOf(Var(client, NoOffset)), AddrOf(Var(manager, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:130:3)
[Warning][Unknown] Unknown address in {&node2} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:130:3)
[Warning][Unknown] Unknown address in {&node1} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:130:3)
[Warning][Unknown] Unknown address in {&client} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:130:3)
[Warning][Unknown] Unknown address in {&manager} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:130:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:130:3)
[Warning][Race] Memory location safe@popl20-commit-2.wvr.c:47:7 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:55:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:73:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:79:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:178:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:97:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:179:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:115:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:180:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:139:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:185:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:55:5)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:73:5)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:79:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:178:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:97:5)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:179:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:115:5)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:180:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:139:5)
[Warning][Race] Memory location client_back@popl20-commit-2.wvr.c:42:32 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:84:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:85:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:86:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:180:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:138:5)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:86:5)
[Warning][Race] Memory location node2_back@popl20-commit-2.wvr.c:45:30 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:66:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:67:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:68:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:179:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:114:5)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:68:5)
[Warning][Race] Memory location node1_back@popl20-commit-2.wvr.c:44:30 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:60:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:61:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:62:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:178:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:96:5)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:62:5)
[Warning][Race] Memory location manager_back@popl20-commit-2.wvr.c:43:34 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:54:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:72:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:177:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:78:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:178:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:102:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:178:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:103:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:178:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:104:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:179:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:120:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:179:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:121:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:179:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:122:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:180:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:132:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:180:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:133:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:180:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:134:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:178:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:104:5)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:179:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:122:5)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:180:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c:134:5)

Summary for all memory locations:
	safe:           15
	vulnerable:      0
	unsafe:          5
	-------------------
	total:          20
t> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Not unwinding loop thread1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 52 function thread1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Unwinding loop thread2.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 94 function thread2 thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Not unwinding loop thread2.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 94 function thread2 thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Unwinding loop thread3.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 112 function thread3 thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Not unwinding loop thread3.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 112 function thread3 thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
Unwinding loop thread4.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 130 function thread4 thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
Not unwinding loop thread4.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c line 130 function thread4 thread 4
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/weaver/popl20-commit-2.wvr.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 102 103 104 105 112 113 114 115 116 120 121 122 123 130 131 132 133 134 135 138 139 140 152 153 157 158 162 163 167 168 172 173 185 186 52 53 54 55 56 60 61 62 63 66 67 68 69 72 73 74 78 79 80 84 85 86 87 94 95 96 97 98 
The number of races before goblint filter: 408
The number of races after goblint filter: 30
Race categories: 12
	158(1) - 87(1) client_back:
		client_back#2 client_back#3
		client_back#2 client_back#5
		client_back#2 client_back#6
		client_back#2 client_back#8
	152(1) - 105(1) manager_size:
		manager_size#2 manager_size#15
		manager_size#2 manager_size#17
	152(1) - 123(1) manager_size:
		manager_size#2 manager_size#19
		manager_size#2 manager_size#21
	152(1) - 135(1) manager_size:
		manager_size#2 manager_size#23
		manager_size#2 manager_size#25
	163(1) - 63(1) node1_back:
		node1_back#2 node1_back#3
		node1_back#2 node1_back#5
		node1_back#2 node1_back#6
		node1_back#2 node1_back#8
	168(1) - 69(1) node2_back:
		node2_back#2 node2_back#3
		node2_back#2 node2_back#5
		node2_back#2 node2_back#6
		node2_back#2 node2_back#8
	172(1) - 105(1) ok:
		ok#2 ok#15
		ok#2 ok#17
	172(1) - 123(1) ok:
		ok#2 ok#19
		ok#2 ok#21
	172(1) - 87(1) ok:
		ok#2 ok#7
		ok#2 ok#13
	173(1) - 135(1) update:
		update#2 update#23
		update#2 update#25
	173(1) - 63(1) update:
		update#2 update#5
		update#2 update#11
	173(1) - 69(1) update:
		update#2 update#7
		update#2 update#13
Runtime Symex: 3.65232s
Adding SC constraints
Shared update: 12R/2W
Shared __CPROVER_threads_exited: 8R/5W
Shared __CPROVER_next_thread_id: 7R/5W
Shared manager: 12R/2W
Shared client: 4R/2W
Shared node1: 4R/2W
Shared node2: 4R/2W
Shared client_size: 4R/2W
Shared client_front: 2R/4W
Shared client_back: 4R/4W
Shared manager_size: 12R/2W
Shared manager_front: 6R/8W
Shared manager_back: 12R/8W
Shared node1_size: 4R/2W
Shared node1_front: 2R/4W
Shared node1_back: 4R/4W
Shared node2_size: 4R/2W
Shared node2_front: 2R/4W
Shared node2_back: 4R/4W
Shared ok: 12R/2W
Shared safe: 14R/14W
Shared main::1::t1!0@1: 2R/2W
Shared main::1::t2!0@1: 2R/2W
Shared main::1::t3!0@1: 2R/2W
Shared main::1::t4!0@1: 2R/2W
Shared symex_dynamic::dynamic_object1: 12R/3W
Shared symex_dynamic::dynamic_object2: 4R/3W
Shared symex_dynamic::dynamic_object3: 4R/3W
Shared symex_dynamic::dynamic_object4: 4R/3W
size of program expression: 2393 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0262227s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0205737s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.0733177s
Solving with Deagle's Closure solver
216273 variables, 78851 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 0.0733686s
Runtime decision procedure: 0.132464s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-commit-2.wvr.c function main
[nodatarace.assertion.0] line 180 No data races on variable client_back between line 158 and line 87: SUCCESS
[nodatarace.assertion.1] line 180 No data races on variable manager_size between line 152 and line 105: SUCCESS
[nodatarace.assertion.2] line 180 No data races on variable manager_size between line 152 and line 123: SUCCESS
[nodatarace.assertion.3] line 180 No data races on variable manager_size between line 152 and line 135: SUCCESS
[nodatarace.assertion.4] line 180 No data races on variable node1_back between line 163 and line 63: SUCCESS
[nodatarace.assertion.5] line 180 No data races on variable node2_back between line 168 and line 69: SUCCESS
[nodatarace.assertion.6] line 180 No data races on variable ok between line 172 and line 105: SUCCESS
[nodatarace.assertion.7] line 180 No data races on variable ok between line 172 and line 123: SUCCESS
[nodatarace.assertion.8] line 180 No data races on variable ok between line 172 and line 87: SUCCESS
[nodatarace.assertion.9] line 180 No data races on variable update between line 173 and line 135: SUCCESS
[nodatarace.assertion.10] line 180 No data races on variable update between line 173 and line 63: SUCCESS
[nodatarace.assertion.11] line 180 No data races on variable update between line 173 and line 69: SUCCESS

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