./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.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-1-dsl.wvr.c
Converting
Type-checking parallel-parallel-sum-1-dsl.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-1-dsl.wvr file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.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
n_1's upper bound is 2147483646
plus::b's upper bound is 0
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-1-dsl.wvr.c line 184 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-1-dsl.wvr.c line 184 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-1-dsl.wvr.c line 184 function create_fresh_int_array 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
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
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-1-dsl.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-1-dsl.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-1-dsl.wvr.c line 48 function thread2 thread 3
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
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-1-dsl.wvr.c line 66 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 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c line 66 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-[Warning][Unknown] Invalidating expressions: AddrOf(Var(n_1,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:155:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(s_2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:156:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i_3, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:157:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t_4, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:158:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t_5, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:159:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(s_6, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:160:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i_7, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:161:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t_8, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:162:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t_9, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:163: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-1-dsl.wvr.c:185:5)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:52:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:48:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:48:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t_9,
                                     NoOffset)), AddrOf(Var(t_8, NoOffset)), AddrOf(Var(i_7, NoOffset)), AddrOf(Var(s_6, NoOffset)), AddrOf(Var(t_5, NoOffset)), AddrOf(Var(t_4, NoOffset)), AddrOf(Var(i_3, NoOffset)), AddrOf(Var(s_2, NoOffset)), AddrOf(Var(n_1, NoOffset)), AddrOf(Var(X_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:48:3)
[Warning][Unknown] Unknown address in {&X_0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:48:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:48:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:70:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:66:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:66:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t_9,
                                     NoOffset)), AddrOf(Var(t_8, NoOffset)), AddrOf(Var(i_7, NoOffset)), AddrOf(Var(s_6, NoOffset)), AddrOf(Var(t_5, NoOffset)), AddrOf(Var(t_4, NoOffset)), AddrOf(Var(i_3, NoOffset)), AddrOf(Var(s_2, NoOffset)), AddrOf(Var(n_1, NoOffset)), AddrOf(Var(X_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:66:3)
[Warning][Unknown] Unknown address in {&X_0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:66:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:66:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:104:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:100:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:100:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t_9,
                                     NoOffset)), AddrOf(Var(t_8, NoOffset)), AddrOf(Var(i_7, NoOffset)), AddrOf(Var(s_6, NoOffset)), AddrOf(Var(t_5, NoOffset)), AddrOf(Var(t_4, NoOffset)), AddrOf(Var(i_3, NoOffset)), AddrOf(Var(s_2, NoOffset)), AddrOf(Var(n_1, NoOffset)), AddrOf(Var(X_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:100:3)
[Warning][Unknown] Unknown address in {&X_0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:100:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:100:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:122:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:118:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:118:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t_9,
                                     NoOffset)), AddrOf(Var(t_8, NoOffset)), AddrOf(Var(i_7, NoOffset)), AddrOf(Var(s_6, NoOffset)), AddrOf(Var(t_5, NoOffset)), AddrOf(Var(t_4, NoOffset)), AddrOf(Var(i_3, NoOffset)), AddrOf(Var(s_2, NoOffset)), AddrOf(Var(n_1, NoOffset)), AddrOf(Var(X_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:118:3)
[Warning][Unknown] Unknown address in {&X_0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:118:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:118:3)
[Warning][Race] Memory location i_7@parallel-parallel-sum-1-dsl.wvr.c:42:35 (race with conf. 110):
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:144:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:102:5)
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:144:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:103:5)
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:144:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:104:5)
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:144:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:111:3)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:145:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:120:5)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:145:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:121:5)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:145:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:122:5)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:145:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:129:3)
  write with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:144:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:103:5)
  write with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:145:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:121:5)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:139:3)
[Warning][Race] Memory location s_6@parallel-parallel-sum-1-dsl.wvr.c:42:30 (race with conf. 110):
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:144:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:107:5)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:145:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:125:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:173:3)
  write with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:144:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:107:5)
  write with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:145:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:125:5)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:170:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:140:3)
[Warning][Race] Memory location s_2@parallel-parallel-sum-1-dsl.wvr.c:42:10 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:92:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:55:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:93:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:73:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:173:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:92:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:55:5)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:93:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:73:5)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:88:3)
[Warning][Race] Memory location i_3@parallel-parallel-sum-1-dsl.wvr.c:42:15 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:92:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:50:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:92:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:51:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:92:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:52:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:92:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:59:3)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:93:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:68:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:93:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:69:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:93:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:70:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:93:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:77:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:92:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:51:5)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:93:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:69:5)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:169:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c:87:3)

Summary for all memory locations:
	safe:            7
	vulnerable:      0
	unsafe:          4
	-------------------
	total:          11
1-dsl.wvr.c line 66 function thread3 thread 4
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
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-1-dsl.wvr.c line 100 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-1-dsl.wvr.c line 100 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-1-dsl.wvr.c line 100 function thread5 thread 5
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
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-1-dsl.wvr.c line 118 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-1-dsl.wvr.c line 118 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-1-dsl.wvr.c line 118 function thread6 thread 6
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-parallel-sum-1-dsl.wvr.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 100 101 102 103 104 105 107 108 111 112 118 119 120 121 122 123 125 126 129 130 139 140 141 155 156 173 174 48 49 50 51 52 53 55 56 59 60 66 67 68 69 70 71 73 74 77 78 87 88 89 
The number of races before goblint filter: 292
The number of races after goblint filter: 57
Race categories: 17
	155(1) - 105(1) n_1:
		n_1#2 n_1#19
		n_1#2 n_1#21
		n_1#2 n_1#23
	155(1) - 112(1) n_1:
		n_1#2 n_1#25
	155(1) - 123(1) n_1:
		n_1#2 n_1#27
		n_1#2 n_1#29
		n_1#2 n_1#31
	155(1) - 130(1) n_1:
		n_1#2 n_1#33
	155(1) - 53(1) n_1:
		n_1#2 n_1#3
		n_1#2 n_1#5
		n_1#2 n_1#7
	155(1) - 60(1) n_1:
		n_1#2 n_1#9
	155(1) - 71(1) n_1:
		n_1#2 n_1#11
		n_1#2 n_1#13
		n_1#2 n_1#15
	155(1) - 78(1) n_1:
		n_1#2 n_1#17
	156(1) - 56(1) s_2:
		s_2#2 s_2#6
		s_2#2 s_2#8
		s_2#2 s_2#9
		s_2#2 s_2#11
		s_2#2 s_2#12
		s_2#2 s_2#14
	156(1) - 74(1) s_2:
		s_2#2 s_2#15
		s_2#2 s_2#17
		s_2#2 s_2#18
		s_2#2 s_2#20
		s_2#2 s_2#21
		s_2#2 s_2#23
	156(1) - 89(1) s_2:
		s_2#2 s_2#5
	173(1) - 56(1) s_2:
		s_2#3 s_2#8
		s_2#3 s_2#11
		s_2#3 s_2#14
		s_2#4 s_2#8
		s_2#4 s_2#11
		s_2#4 s_2#14
	173(1) - 74(1) s_2:
		s_2#3 s_2#17
		s_2#3 s_2#20
		s_2#3 s_2#23
		s_2#4 s_2#17
		s_2#4 s_2#20
		s_2#4 s_2#23
	173(1) - 89(1) s_2:
		s_2#3 s_2#5
		s_2#4 s_2#5
	173(1) - 108(1) s_6:
		s_6#3 s_6#8
		s_6#3 s_6#11
		s_6#3 s_6#14
		s_6#4 s_6#8
		s_6#4 s_6#11
		s_6#4 s_6#14
	173(1) - 126(1) s_6:
		s_6#3 s_6#17
		s_6#3 s_6#20
		s_6#3 s_6#23
		s_6#4 s_6#17
		s_6#4 s_6#20
		s_6#4 s_6#23
	173(1) - 141(1) s_6:
		s_6#3 s_6#5
		s_6#4 s_6#5
Runtime Symex: 2.07033s
Adding SC constraints
Shared __CPROVER_threads_exited: 12R/7W
Shared __CPROVER_next_thread_id: 11R/7W
Shared X_0: 12R/2W
Shared n_1: 16R/2W
Shared s_2: 8R/9W
Shared i_3: 8R/9W
Shared t_4: 3R/5W
Shared t_5: 3R/5W
Shared s_6: 8R/9W
Shared i_7: 8R/9W
Shared t_8: 3R/5W
Shared t_9: 3R/5W
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: 2257 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.016525s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0218941s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.139303s
Solving with Deagle's Closure solver
222103 variables, 936019 clauses
ClosureSolver finishes with 10359 conflicts, 1353437 decisions, and 10639875 propagations. 11130 theory propagations and 525 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 2.20814s
Runtime decision procedure: 2.25635s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1-dsl.wvr.c function thread4
[nodatarace.assertion.0] line 145 No data races on variable n_1 between line 155 and line 105: SUCCESS
[nodatarace.assertion.1] line 145 No data races on variable n_1 between line 155 and line 112: SUCCESS
[nodatarace.assertion.2] line 145 No data races on variable n_1 between line 155 and line 123: SUCCESS
[nodatarace.assertion.3] line 145 No data races on variable n_1 between line 155 and line 130: SUCCESS
[nodatarace.assertion.4] line 145 No data races on variable n_1 between line 155 and line 53: SUCCESS
[nodatarace.assertion.5] line 145 No data races on variable n_1 between line 155 and line 60: SUCCESS
[nodatarace.assertion.6] line 145 No data races on variable n_1 between line 155 and line 71: SUCCESS
[nodatarace.assertion.7] line 145 No data races on variable n_1 between line 155 and line 78: SUCCESS
[nodatarace.assertion.8] line 145 No data races on variable s_2 between line 156 and line 56: SUCCESS
[nodatarace.assertion.9] line 145 No data races on variable s_2 between line 156 and line 74: SUCCESS
[nodatarace.assertion.10] line 145 No data races on variable s_2 between line 156 and line 89: SUCCESS
[nodatarace.assertion.11] line 145 No data races on variable s_2 between line 173 and line 56: SUCCESS
[nodatarace.assertion.12] line 145 No data races on variable s_2 between line 173 and line 74: SUCCESS
[nodatarace.assertion.13] line 145 No data races on variable s_2 between line 173 and line 89: SUCCESS
[nodatarace.assertion.14] line 145 No data races on variable s_6 between line 173 and line 108: SUCCESS
[nodatarace.assertion.15] line 145 No data races on variable s_6 between line 173 and line 126: SUCCESS
[nodatarace.assertion.16] line 145 No data races on variable s_6 between line 173 and line 141: SUCCESS

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