./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-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/parallel-parallel-sum-2.wvr.c
Converting
Type-checking parallel-parallel-sum-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 parallel-parallel-sum-2.wvr file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-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 6 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
plus::b's upper bound is 0
n's upper bound is 2147483646
Use SV-COMP unwinding strategy: 3
Deagle's solver is set!!!!!!
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
Unwinding loop create_fresh_int_array.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 176 function create_fresh_int_array thread 0
Unwinding loop create_fresh_int_array.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 176 function create_fresh_int_array thread 0
Not unwinding loop create_fresh_int_array.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 176 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 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 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 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
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 recursion __spawned_thread iteration 1
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 thread2.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 48 function thread2 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
Unwinding loop thread2.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 48 function thread2 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 thread2.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 48 function thread2 thread 3
Unwinding recursion __spawned_thread iteration 1
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 thread3.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 63 function thread3 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
Unwinding loop thread3.0 iterati[Warning][Unknown] Invalidating expressions: AddrOf(Var(i1,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:143:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:144:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t11, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:145:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t21, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:146:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t12, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:147:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t22, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:148:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(s11, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:149:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(s21, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:150:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(s22, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:151:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(x1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:152:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(x2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:153:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:154:3)
[Warning][Unknown] Invalidating expressions: IndexPI(Lval(Var(arr, NoOffset)), Lval(Var(i, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:177:5)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:52:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:48:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:48:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n,
                                     NoOffset)), AddrOf(Var(x2, NoOffset)), AddrOf(Var(x1, NoOffset)), AddrOf(Var(s22, NoOffset)), AddrOf(Var(s12, NoOffset)), AddrOf(Var(s21, NoOffset)), AddrOf(Var(s11, NoOffset)), AddrOf(Var(t22, NoOffset)), AddrOf(Var(t12, NoOffset)), AddrOf(Var(t21, NoOffset)), AddrOf(Var(t11, NoOffset)), AddrOf(Var(i2, NoOffset)), AddrOf(Var(i1, NoOffset)), AddrOf(Var(x, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:48:3)
[Warning][Unknown] Unknown address in {&x} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:48:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:48:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:67:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:63:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:63:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n,
                                     NoOffset)), AddrOf(Var(x2, NoOffset)), AddrOf(Var(x1, NoOffset)), AddrOf(Var(s22, NoOffset)), AddrOf(Var(s12, NoOffset)), AddrOf(Var(s21, NoOffset)), AddrOf(Var(s11, NoOffset)), AddrOf(Var(t22, NoOffset)), AddrOf(Var(t12, NoOffset)), AddrOf(Var(t21, NoOffset)), AddrOf(Var(t11, NoOffset)), AddrOf(Var(i2, NoOffset)), AddrOf(Var(i1, NoOffset)), AddrOf(Var(x, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:63:3)
[Warning][Unknown] Unknown address in {&x} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:63:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:63:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:98:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:94:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:94:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n,
                                     NoOffset)), AddrOf(Var(x2, NoOffset)), AddrOf(Var(x1, NoOffset)), AddrOf(Var(s22, NoOffset)), AddrOf(Var(s12, NoOffset)), AddrOf(Var(s21, NoOffset)), AddrOf(Var(s11, NoOffset)), AddrOf(Var(t22, NoOffset)), AddrOf(Var(t12, NoOffset)), AddrOf(Var(t21, NoOffset)), AddrOf(Var(t11, NoOffset)), AddrOf(Var(i2, NoOffset)), AddrOf(Var(i1, NoOffset)), AddrOf(Var(x, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:94:3)
[Warning][Unknown] Unknown address in {&x} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:94:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:94:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:113:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:109:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:109:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n,
                                     NoOffset)), AddrOf(Var(x2, NoOffset)), AddrOf(Var(x1, NoOffset)), AddrOf(Var(s22, NoOffset)), AddrOf(Var(s12, NoOffset)), AddrOf(Var(s21, NoOffset)), AddrOf(Var(s11, NoOffset)), AddrOf(Var(t22, NoOffset)), AddrOf(Var(t12, NoOffset)), AddrOf(Var(t21, NoOffset)), AddrOf(Var(t11, NoOffset)), AddrOf(Var(i2, NoOffset)), AddrOf(Var(i1, NoOffset)), AddrOf(Var(x, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:109:3)
[Warning][Unknown] Unknown address in {&x} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:109:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:109:3)
[Warning][Race] Memory location s22@parallel-parallel-sum-2.wvr.c:42:48 (race with conf. 110):
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:128:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:116:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:133:3)
  write with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:128:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:116:5)
[Warning][Race] Memory location s11@parallel-parallel-sum-2.wvr.c:42:33 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:81:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:55:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:87:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:81:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:55:5)
[Warning][Race] Memory location s12@parallel-parallel-sum-2.wvr.c:42:43 (race with conf. 110):
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:127:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:101:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:133:3)
  write with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:127:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:101:5)
[Warning][Race] Memory location x1@parallel-parallel-sum-2.wvr.c:42:53 (race with conf. 110):
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:165:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:87:3)
[Warning][Race] Memory location x2@parallel-parallel-sum-2.wvr.c:42:57 (race with conf. 110):
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:165:3)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:133:3)
[Warning][Race] Memory location s21@parallel-parallel-sum-2.wvr.c:42:38 (race with conf. 110):
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:82:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:70:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:87:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:82:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:70:5)
[Warning][Race] Memory location i2@parallel-parallel-sum-2.wvr.c:42:9 (race with conf. 110):
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:127:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:96:5)
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:127:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:97:5)
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:127:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:98:5)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:128:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:111:5)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:128:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:112:5)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:128:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:113:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:131:3)
  write with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:127:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:97:5)
  write with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:128:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:162:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:112:5)
[Warning][Race] Memory location i1@parallel-parallel-sum-2.wvr.c:42:5 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:81:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:50:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:81:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:51:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:81:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:52:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:82:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:65:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:82:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:66:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:82:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:67:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:85:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:81:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:51:5)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:82:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:66:5)

Summary for all memory locations:
	safe:            7
	vulnerable:      0
	unsafe:          8
	-------------------
	total:          15
on 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 63 function thread3 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 thread3.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 63 function thread3 thread 4
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
Unwinding loop thread5.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 94 function thread5 thread 5
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
Unwinding loop thread5.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 94 function thread5 thread 5
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
Not unwinding loop thread5.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 94 function thread5 thread 5
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
Unwinding loop thread6.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 109 function thread6 thread 6
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
Unwinding loop thread6.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 109 function thread6 thread 6
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
Not unwinding loop thread6.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c line 109 function thread6 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-parallel-sum-2.wvr.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 101 102 109 110 111 112 113 114 116 117 131 132 133 134 143 144 165 166 48 49 50 51 52 53 55 56 63 64 65 66 67 68 70 71 85 86 87 88 94 95 96 97 98 99 
The number of races before goblint filter: 289
The number of races after goblint filter: 56
Race categories: 12
	143(1) - 53(1) i1:
		i1#2 i1#5
		i1#2 i1#7
		i1#2 i1#8
		i1#2 i1#10
		i1#2 i1#11
		i1#2 i1#13
	143(1) - 68(1) i1:
		i1#2 i1#14
		i1#2 i1#16
		i1#2 i1#17
		i1#2 i1#19
		i1#2 i1#20
		i1#2 i1#22
	143(1) - 85(1) i1:
		i1#2 i1#3
		i1#2 i1#4
	85(1) - 53(1) i1:
		i1#3 i1#7
		i1#3 i1#10
		i1#3 i1#13
		i1#4 i1#7
		i1#4 i1#10
		i1#4 i1#13
	85(1) - 68(1) i1:
		i1#3 i1#16
		i1#3 i1#19
		i1#3 i1#22
		i1#4 i1#16
		i1#4 i1#19
		i1#4 i1#22
	131(1) - 114(1) i2:
		i2#3 i2#16
		i2#3 i2#19
		i2#3 i2#22
		i2#4 i2#16
		i2#4 i2#19
		i2#4 i2#22
	131(1) - 99(1) i2:
		i2#3 i2#7
		i2#3 i2#10
		i2#3 i2#13
		i2#4 i2#7
		i2#4 i2#10
		i2#4 i2#13
	144(1) - 114(1) i2:
		i2#2 i2#14
		i2#2 i2#16
		i2#2 i2#17
		i2#2 i2#19
		i2#2 i2#20
		i2#2 i2#22
	144(1) - 131(1) i2:
		i2#2 i2#3
		i2#2 i2#4
	144(1) - 99(1) i2:
		i2#2 i2#5
		i2#2 i2#7
		i2#2 i2#8
		i2#2 i2#10
		i2#2 i2#11
		i2#2 i2#13
	165(1) - 88(1) x1:
		x1#3 x1#5
		x1#4 x1#5
	165(1) - 134(1) x2:
		x2#3 x2#5
		x2#4 x2#5
Runtime Symex: 2.47412s
Adding SC constraints
Shared __CPROVER_threads_exited: 12R/7W
Shared __CPROVER_next_thread_id: 11R/7W
Shared x: 12R/2W
Shared i1: 8R/8W
Shared i2: 8R/8W
Shared t11: 3R/5W
Shared t21: 3R/5W
Shared t12: 3R/5W
Shared t22: 3R/5W
Shared s11: 4R/5W
Shared s21: 4R/5W
Shared s12: 4R/4W
Shared s22: 4R/5W
Shared x1: 2R/3W
Shared x2: 2R/3W
Shared n: 16R/2W
Shared main::1::t1!0@1: 2R/2W
Shared main::1::t4!0@1: 2R/2W
Shared symex_dynamic::dynamic_object1: 12R/4W
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: 2223 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0142539s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0238886s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.141665s
Solving with Deagle's Closure solver
222549 variables, 933674 clauses
ClosureSolver finishes with 9650 conflicts, 1851611 decisions, and 11116199 propagations. 7831 theory propagations and 409 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 2.00927s
Runtime decision procedure: 2.06069s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c function thread4
[nodatarace.assertion.0] line 128 No data races on variable i1 between line 143 and line 53: SUCCESS
[nodatarace.assertion.1] line 128 No data races on variable i1 between line 143 and line 68: SUCCESS
[nodatarace.assertion.2] line 128 No data races on variable i1 between line 143 and line 85: SUCCESS
[nodatarace.assertion.3] line 128 No data races on variable i1 between line 85 and line 53: SUCCESS
[nodatarace.assertion.4] line 128 No data races on variable i1 between line 85 and line 68: SUCCESS
[nodatarace.assertion.5] line 128 No data races on variable i2 between line 131 and line 114: SUCCESS
[nodatarace.assertion.6] line 128 No data races on variable i2 between line 131 and line 99: SUCCESS
[nodatarace.assertion.7] line 128 No data races on variable i2 between line 144 and line 114: SUCCESS
[nodatarace.assertion.8] line 128 No data races on variable i2 between line 144 and line 131: SUCCESS
[nodatarace.assertion.9] line 128 No data races on variable i2 between line 144 and line 99: SUCCESS
[nodatarace.assertion.10] line 128 No data races on variable x1 between line 165 and line 88: SUCCESS
[nodatarace.assertion.11] line 128 No data races on variable x2 between line 165 and line 134: SUCCESS

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