./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.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-barrier.wvr.c
Converting
Type-checking parallel-barrier.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-barrier.wvr file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.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 6 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
[Warning][Unknown] Invalidating expressions: AddrOf(Var(x_0,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:176:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(y_1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:177:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:178:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:178:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(y_7, NoOffset)), AddrOf(Var(temp_11, NoOffset)), AddrOf(Var(temp_10, NoOffset)), AddrOf(Var(f2_9, NoOffset)), AddrOf(Var(f1_8, NoOffset)), AddrOf(Var(x_7, NoOffset)), AddrOf(Var(x_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:178:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f1_2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:178:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:179:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:179:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(y_7, NoOffset)), AddrOf(Var(temp_11, NoOffset)), AddrOf(Var(temp_10, NoOffset)), AddrOf(Var(f2_9, NoOffset)), AddrOf(Var(f1_8, NoOffset)), AddrOf(Var(x_7, NoOffset)), AddrOf(Var(x_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:179:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f2_3, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:179:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_4, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:180:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_5, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:181:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(x_6, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:182:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(x_7, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:183:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:184:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:184:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(y_7, NoOffset)), AddrOf(Var(temp_11, NoOffset)), AddrOf(Var(temp_10, NoOffset)), AddrOf(Var(f2_9, NoOffset)), AddrOf(Var(f1_8, NoOffset)), AddrOf(Var(x_7, NoOffset)), AddrOf(Var(x_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:184:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f1_8, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:184:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:185:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:185:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(y_7, NoOffset)), AddrOf(Var(temp_11, NoOffset)), AddrOf(Var(temp_10, NoOffset)), AddrOf(Var(f2_9, NoOffset)), AddrOf(Var(f1_8, NoOffset)), AddrOf(Var(x_7, NoOffset)), AddrOf(Var(x_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:185:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f2_9, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:185:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_10, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:186:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_11, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:187:3)
[Warning][Race] Memory location f1_2@parallel-barrier.wvr.c:39:7 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:102:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:58:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:103:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:83:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:99:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:102:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:55:3)
[Warning][Race] Memory location f1_8@parallel-barrier.wvr.c:42:7 (race with conf. 110):
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:165:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:121:3)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:166:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:146:3)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:162:3)
  write with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:165:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:118:3)
[Warning][Race] Memory location f2_9@parallel-barrier.wvr.c:42:13 (race with conf. 110):
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:165:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:121:3)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:166:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:146:3)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:162:3)
  write with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:166:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:143:3)
[Warning][Race] Memory location f2_3@parallel-barrier.wvr.c:39:13 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:102:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:58:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:103:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:83:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:99:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:103:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:80:3)
[Warning][Race] Memory location x_0@parallel-barrier.wvr.c:38:5 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:102:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:48:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:103:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:87:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:99:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:197:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:102:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:51:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:103:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:90:3)
[Warning][Race] Memory location y_7@parallel-barrier.wvr.c:44:5 (race with conf. 110):
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:165:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:125:3)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:166:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:136:3)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:162:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:197:3)
  write with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:165:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:128:3)
  write with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:166:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:139:3)
[Warning][Race] Memory location y_1@parallel-barrier.wvr.c:38:10 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:102:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:62:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:103:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:73:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:99:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:197:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:102:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:65:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:103:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:193:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:76:3)
[Warning][Race] Memory location x_6@parallel-barrier.wvr.c:41:5 (race with conf. 110):
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:165:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:111:3)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:166:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:150:3)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:162:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:197:3)
  write with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:165:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:114:3)
  write with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:166:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:194:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:153:3)

Summary for all memory locations:
	safe:            4
	vulnerable:      0
	unsafe:          8
	-------------------
	total:          12
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
Unwinding recursion pthread_create iteration 1
Unwinding recursion pthread_create iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Unwinding recursion pthread_create iteration 1
Unwinding recursion pthread_create iteration 1
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
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-barrier.wvr.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 100 111 112 114 115 118 119 121 122 125 126 128 129 136 137 139 140 143 144 146 147 150 151 153 154 162 163 176 177 197 198 48 49 51 52 55 56 58 59 62 63 65 66 73 74 76 77 80 81 83 84 87 88 90 91 99 
The number of races before goblint filter: 154
The number of races after goblint filter: 52
Race categories: 30
	99(1) - 56(1) f1_2:
		f1_2#3 f1_2#5
		f1_2#4 f1_2#5
	162(1) - 119(1) f1_8:
		f1_8#3 f1_8#5
		f1_8#4 f1_8#5
	99(1) - 81(1) f2_3:
		f2_3#3 f2_3#7
		f2_3#4 f2_3#7
	162(1) - 144(1) f2_9:
		f2_9#3 f2_9#7
		f2_9#4 f2_9#7
	176(1) - 49(1) x_0:
		x_0#2 x_0#7
	176(1) - 52(1) x_0:
		x_0#2 x_0#9
	176(1) - 88(1) x_0:
		x_0#2 x_0#10
	176(1) - 91(1) x_0:
		x_0#2 x_0#12
	176(1) - 99(1) x_0:
		x_0#2 x_0#5
		x_0#2 x_0#6
	197(1) - 52(1) x_0:
		x_0#3 x_0#9
		x_0#4 x_0#9
	197(1) - 91(1) x_0:
		x_0#3 x_0#12
		x_0#4 x_0#12
	99(1) - 52(1) x_0:
		x_0#5 x_0#9
		x_0#6 x_0#9
	99(1) - 91(1) x_0:
		x_0#5 x_0#12
		x_0#6 x_0#12
	162(1) - 115(1) x_6:
		x_6#5 x_6#9
		x_6#6 x_6#9
	162(1) - 154(1) x_6:
		x_6#5 x_6#12
		x_6#6 x_6#12
	197(1) - 115(1) x_6:
		x_6#3 x_6#9
		x_6#4 x_6#9
	197(1) - 154(1) x_6:
		x_6#3 x_6#12
		x_6#4 x_6#12
	177(1) - 63(1) y_1:
		y_1#2 y_1#7
	177(1) - 66(1) y_1:
		y_1#2 y_1#9
	177(1) - 74(1) y_1:
		y_1#2 y_1#10
	177(1) - 77(1) y_1:
		y_1#2 y_1#12
	177(1) - 99(1) y_1:
		y_1#2 y_1#5
		y_1#2 y_1#6
	197(1) - 66(1) y_1:
		y_1#3 y_1#9
		y_1#4 y_1#9
	197(1) - 77(1) y_1:
		y_1#3 y_1#12
		y_1#4 y_1#12
	99(1) - 66(1) y_1:
		y_1#5 y_1#9
		y_1#6 y_1#9
	99(1) - 77(1) y_1:
		y_1#5 y_1#12
		y_1#6 y_1#12
	162(1) - 129(1) y_7:
		y_7#4 y_7#8
		y_7#5 y_7#8
	162(1) - 140(1) y_7:
		y_7#4 y_7#11
		y_7#5 y_7#11
	197(1) - 129(1) y_7:
		y_7#2 y_7#8
		y_7#3 y_7#8
	197(1) - 140(1) y_7:
		y_7#2 y_7#11
		y_7#3 y_7#11
Runtime Symex: 1.38445s
Adding SC constraints
Shared __CPROVER_threads_exited: 12R/7W
Shared __CPROVER_next_thread_id: 11R/7W
Shared x_0: 6R/4W
Shared y_1: 6R/4W
Shared f1_2: 4R/3W
Shared f2_3: 4R/3W
Shared temp_4: 2R/4W
Shared temp_5: 2R/4W
Shared x_6: 6R/4W
Shared f1_8: 4R/3W
Shared f2_9: 4R/3W
Shared temp_10: 2R/4W
Shared temp_11: 2R/4W
Shared y_7: 6R/3W
Shared main::1::t1!0@1: 2R/2W
Shared main::1::t4!0@1: 2R/2W
Shared thread1::1::t2!1@1: 2R/3W
Shared thread1::1::t3!1@1: 2R/3W
Shared thread4::1::t5!2@1: 2R/3W
Shared thread4::1::t6!2@1: 2R/3W
size of program expression: 1274 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0070399s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00849438s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.0135039s
Solving with Deagle's Closure solver
19910 variables, 67152 clauses
ClosureSolver finishes with 10237 conflicts, 19647 decisions, and 9557527 propagations. 12110 theory propagations and 441 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 1.74442s
Runtime decision procedure: 1.77185s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c function thread4
[nodatarace.assertion.0] line 166 No data races on variable f1_2 between line 99 and line 56: SUCCESS
[nodatarace.assertion.1] line 166 No data races on variable f1_8 between line 162 and line 119: SUCCESS
[nodatarace.assertion.2] line 166 No data races on variable f2_3 between line 99 and line 81: SUCCESS
[nodatarace.assertion.3] line 166 No data races on variable f2_9 between line 162 and line 144: SUCCESS
[nodatarace.assertion.4] line 166 No data races on variable x_0 between line 176 and line 49: SUCCESS
[nodatarace.assertion.5] line 166 No data races on variable x_0 between line 176 and line 52: SUCCESS
[nodatarace.assertion.6] line 166 No data races on variable x_0 between line 176 and line 88: SUCCESS
[nodatarace.assertion.7] line 166 No data races on variable x_0 between line 176 and line 91: SUCCESS
[nodatarace.assertion.8] line 166 No data races on variable x_0 between line 176 and line 99: SUCCESS
[nodatarace.assertion.9] line 166 No data races on variable x_0 between line 197 and line 52: SUCCESS
[nodatarace.assertion.10] line 166 No data races on variable x_0 between line 197 and line 91: SUCCESS
[nodatarace.assertion.11] line 166 No data races on variable x_0 between line 99 and line 52: SUCCESS
[nodatarace.assertion.12] line 166 No data races on variable x_0 between line 99 and line 91: SUCCESS
[nodatarace.assertion.13] line 166 No data races on variable x_6 between line 162 and line 115: SUCCESS
[nodatarace.assertion.14] line 166 No data races on variable x_6 between line 162 and line 154: SUCCESS
[nodatarace.assertion.15] line 166 No data races on variable x_6 between line 197 and line 115: SUCCESS
[nodatarace.assertion.16] line 166 No data races on variable x_6 between line 197 and line 154: SUCCESS
[nodatarace.assertion.17] line 166 No data races on variable y_1 between line 177 and line 63: SUCCESS
[nodatarace.assertion.18] line 166 No data races on variable y_1 between line 177 and line 66: SUCCESS
[nodatarace.assertion.19] line 166 No data races on variable y_1 between line 177 and line 74: SUCCESS
[nodatarace.assertion.20] line 166 No data races on variable y_1 between line 177 and line 77: SUCCESS
[nodatarace.assertion.21] line 166 No data races on variable y_1 between line 177 and line 99: SUCCESS
[nodatarace.assertion.22] line 166 No data races on variable y_1 between line 197 and line 66: SUCCESS
[nodatarace.assertion.23] line 166 No data races on variable y_1 between line 197 and line 77: SUCCESS
[nodatarace.assertion.24] line 166 No data races on variable y_1 between line 99 and line 66: SUCCESS
[nodatarace.assertion.25] line 166 No data races on variable y_1 between line 99 and line 77: SUCCESS
[nodatarace.assertion.26] line 166 No data races on variable y_7 between line 162 and line 129: SUCCESS
[nodatarace.assertion.27] line 166 No data races on variable y_7 between line 162 and line 140: SUCCESS
[nodatarace.assertion.28] line 166 No data races on variable y_7 between line 197 and line 129: SUCCESS
[nodatarace.assertion.29] line 166 No data races on variable y_7 between line 197 and line 140: SUCCESS

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