./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.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/parallel-bakery-3.wvr.c
Converting
Type-checking parallel-bakery-3.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 parallel-bakery-3.wvr file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.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 3 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:174:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:174:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i3,
                                     NoOffset)), AddrOf(Var(i2, NoOffset)), AddrOf(Var(i1, NoOffset)), AddrOf(Var(i, NoOffset)), AddrOf(Var(n3, NoOffset)), AddrOf(Var(n2, NoOffset)), AddrOf(Var(n1, NoOffset)), AddrOf(Var(e3, NoOffset)), AddrOf(Var(e2, NoOffset)), AddrOf(Var(e1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:174:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(e1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:174:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:175:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:175:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i3, NoOffset)), AddrOf(Var(i2, NoOffset)), AddrOf(Var(i1, NoOffset)), AddrOf(Var(i, NoOffset)), AddrOf(Var(n3, NoOffset)), AddrOf(Var(n2, NoOffset)), AddrOf(Var(n1, NoOffset)), AddrOf(Var(e3, NoOffset)), AddrOf(Var(e2, NoOffset)), AddrOf(Var(e1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:175:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(e2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:175:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:176:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:176:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i3, NoOffset)), AddrOf(Var(i2, NoOffset)), AddrOf(Var(i1, NoOffset)), AddrOf(Var(i, NoOffset)), AddrOf(Var(n3, NoOffset)), AddrOf(Var(n2, NoOffset)), AddrOf(Var(n1, NoOffset)), AddrOf(Var(e3, NoOffset)), AddrOf(Var(e2, NoOffset)), AddrOf(Var(e1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:176:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(e3, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:176:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:177:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:178:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n3, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:179:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:180:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:181:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:182:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i3, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:183:3)
[Warning][Race] Memory location e3@parallel-bakery-3.wvr.c:38:15 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:65:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:108:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:129:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:141:3)
[Warning][Race] Memory location e1@parallel-bakery-3.wvr.c:38:7 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:102:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:145:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:43:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:55:3)
[Warning][Race] Memory location e2@parallel-bakery-3.wvr.c:38:11 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:59:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:151:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:86:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:98:3)
[Warning][Race] Memory location n1@parallel-bakery-3.wvr.c:39:5 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:46:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:49:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:52:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:62:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:68:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:89:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:105:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:132:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:148:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:46:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:49:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:52:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:78:3)
[Warning][Race] Memory location i@parallel-bakery-3.wvr.c:39:17 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:72:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:115:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:158:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:195:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:75:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:118:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:161:3)
[Warning][Race] Memory location n3@parallel-bakery-3.wvr.c:39:13 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:49:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:68:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:92:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:111:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:132:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:135:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:138:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:148:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:154:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:132:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:135:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:138:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:164:3)
[Warning][Race] Memory location n2@parallel-bakery-3.wvr.c:39:9 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:46:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:189:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:62:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:89:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:92:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:95:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:105:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:111:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:135:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:191:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:154:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:89:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:92:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:95:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:190:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c:121:3)

Summary for all memory locations:
	safe:            3
	vulnerable:      0
	unsafe:          7
	-------------------
	total:          10
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 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 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
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
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
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/parallel-bakery-3.wvr.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 102 103 105 106 108 109 111 112 115 116 118 119 121 122 129 130 132 133 135 136 138 139 141 142 145 146 148 149 151 152 154 155 158 159 161 162 164 165 174 175 195 196 43 44 46 47 49 50 52 53 55 56 59 60 62 63 65 66 68 69 72 73 75 76 78 79 86 87 89 90 92 93 95 96 98 99 
The number of races before goblint filter: 132
The number of races after goblint filter: 14
Race categories: 11
	174(1) - 103(1) e1:
		e1#2 e1#5
	174(1) - 146(1) e1:
		e1#2 e1#7
	174(1) - 44(1) e1:
		e1#2 e1#3
	174(1) - 56(1) e1:
		e1#2 e1#4
	175(1) - 152(1) e2:
		e2#2 e2#7
	175(1) - 60(1) e2:
		e2#2 e2#3
	175(1) - 87(1) e2:
		e2#2 e2#5
	175(1) - 99(1) e2:
		e2#2 e2#6
	195(1) - 119(1) i:
		i#3 i#10
		i#4 i#10
	195(1) - 162(1) i:
		i#3 i#13
		i#4 i#13
	195(1) - 76(1) i:
		i#3 i#7
		i#4 i#7
Runtime Symex: 0.776692s
Adding SC constraints
Shared __CPROVER_threads_exited: 6R/4W
Shared __CPROVER_next_thread_id: 5R/4W
Shared e1: 2R/4W
Shared e2: 2R/4W
Shared e3: 2R/4W
Shared n1: 9R/6W
Shared n2: 9R/6W
Shared n3: 9R/6W
Shared i: 5R/5W
Shared i1: 1R/3W
Shared i2: 1R/3W
Shared i3: 1R/3W
Shared main::1::t1!0@1: 2R/2W
Shared main::1::t2!0@1: 2R/2W
Shared main::1::t3!0@1: 2R/2W
size of program expression: 951 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.00449841s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00687911s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.00205684s
Solving with Deagle's Closure solver
11323 variables, 37012 clauses
ClosureSolver finishes with 47 conflicts, 146 decisions, and 19999 propagations. 150 theory propagations and 8 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.0062581s
Runtime decision procedure: 0.026911s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-3.wvr.c function main
[nodatarace.assertion.0] line 191 No data races on variable e1 between line 174 and line 103: SUCCESS
[nodatarace.assertion.1] line 191 No data races on variable e1 between line 174 and line 146: SUCCESS
[nodatarace.assertion.2] line 191 No data races on variable e1 between line 174 and line 44: SUCCESS
[nodatarace.assertion.3] line 191 No data races on variable e1 between line 174 and line 56: SUCCESS
[nodatarace.assertion.4] line 191 No data races on variable e2 between line 175 and line 152: SUCCESS
[nodatarace.assertion.5] line 191 No data races on variable e2 between line 175 and line 60: SUCCESS
[nodatarace.assertion.6] line 191 No data races on variable e2 between line 175 and line 87: SUCCESS
[nodatarace.assertion.7] line 191 No data races on variable e2 between line 175 and line 99: SUCCESS
[nodatarace.assertion.8] line 191 No data races on variable i between line 195 and line 119: SUCCESS
[nodatarace.assertion.9] line 191 No data races on variable i between line 195 and line 162: SUCCESS
[nodatarace.assertion.10] line 191 No data races on variable i between line 195 and line 76: SUCCESS

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