./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.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.wvr.c
Converting
Type-checking parallel-parallel-sum-1.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.wvr file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 22
signed int (pthread_t *, const pthread_attr_t *, void * (*)(void *), void *)
new definition in module <built-in-library> file <builtin-library-pthread_create> line 20
signed int (pthread_t *thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
Removal of function pointers and virtual functions
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 4 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
n'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.wvr.c line 146 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.wvr.c line 146 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.wvr.c line 146 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
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Unwinding loop thread1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 48 function thread1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Unwinding loop thread1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 48 function thread1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Not unwinding loop thread1.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 48 function thread1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Unwinding loop thread2.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 63 function thread2 thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Unwinding loop thread2.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 63 function thread2 thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Not unwinding loop thread2.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 63 function thread2 thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort threa[Warning][Unknown] Invalidating expressions: AddrOf(Var(i1,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:111:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:112:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t11, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:113:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t21, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:114:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t12, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:115:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(t22, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:116:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(s1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:117:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(s2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:118:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:119: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.wvr.c:147:5)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.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.wvr.c:48:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:48:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n,
                                     NoOffset)), AddrOf(Var(s2, NoOffset)), AddrOf(Var(s1, 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-1.wvr.c:48:3)
[Warning][Unknown] Unknown address in {&x} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:48:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.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.wvr.c:67:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:63:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:63:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n,
                                     NoOffset)), AddrOf(Var(s2, NoOffset)), AddrOf(Var(s1, 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-1.wvr.c:63:3)
[Warning][Unknown] Unknown address in {&x} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:63:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:63:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:82:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:78:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:78:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n,
                                     NoOffset)), AddrOf(Var(s2, NoOffset)), AddrOf(Var(s1, 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-1.wvr.c:78:3)
[Warning][Unknown] Unknown address in {&x} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:78:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:78:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:97:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:93:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:93:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n,
                                     NoOffset)), AddrOf(Var(s2, NoOffset)), AddrOf(Var(s1, 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-1.wvr.c:93:3)
[Warning][Unknown] Unknown address in {&x} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:93:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:93:3)
[Warning][Race] Memory location s1@parallel-parallel-sum-1.wvr.c:42:33 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:127:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:55:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:128:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:70:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:135:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:127:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:55:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:128:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:70:5)
[Warning][Race] Memory location s2@parallel-parallel-sum-1.wvr.c:42:37 (race with conf. 110):
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:129:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:85:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:130:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:100:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:135:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:129:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:85:5)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:130:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:100:5)
[Warning][Race] Memory location i2@parallel-parallel-sum-1.wvr.c:42:9 (race with conf. 110):
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:129:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:80:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:129:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:81:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:129:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:82:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:130:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:95:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:130:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:96:5)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:130:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:97:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:135:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:129:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:81:5)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:130:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:96:5)
[Warning][Race] Memory location i1@parallel-parallel-sum-1.wvr.c:42:5 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:127:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:50:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:127:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:51:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:127:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:52:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:128:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:65:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:128:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:66:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:128:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:67:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:135:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:127:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:51:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:128:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c:66:5)

Summary for all memory locations:
	safe:            7
	vulnerable:      0
	unsafe:          4
	-------------------
	total:          11
d 3
Unwinding loop thread3.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 78 function thread3 thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Unwinding loop thread3.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 78 function thread3 thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Not unwinding loop thread3.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 78 function thread3 thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
Unwinding loop thread4.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 93 function thread4 thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
Unwinding loop thread4.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 93 function thread4 thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
Not unwinding loop thread4.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c line 93 function thread4 thread 4
Handling datarace, passing the problem to goblint first
getcwd: /mnt/goblint-svcomp/benchexec/tools-pldi/deagle
/mnt/goblint-svcomp/benchexec/tools-pldi/deagle/goblint/goblint /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 100 101 111 112 135 136 48 49 50 51 52 53 55 56 63 64 65 66 67 68 70 71 78 79 80 81 82 83 85 86 93 94 95 96 97 98 
The number of races before goblint filter: 300
The number of races after goblint filter: 84
Race categories: 12
	111(1) - 53(1) i1:
		i1#2 i1#7
		i1#2 i1#9
		i1#2 i1#10
		i1#2 i1#12
		i1#2 i1#13
		i1#2 i1#15
	111(1) - 68(1) i1:
		i1#2 i1#16
		i1#2 i1#18
		i1#2 i1#19
		i1#2 i1#21
		i1#2 i1#22
		i1#2 i1#24
	135(1) - 53(1) i1:
		i1#3 i1#9
		i1#3 i1#12
		i1#3 i1#15
		i1#4 i1#9
		i1#4 i1#12
		i1#4 i1#15
		i1#5 i1#9
		i1#5 i1#12
		i1#5 i1#15
		i1#6 i1#9
		i1#6 i1#12
		i1#6 i1#15
	135(1) - 68(1) i1:
		i1#3 i1#18
		i1#3 i1#21
		i1#3 i1#24
		i1#4 i1#18
		i1#4 i1#21
		i1#4 i1#24
		i1#5 i1#18
		i1#5 i1#21
		i1#5 i1#24
		i1#6 i1#18
		i1#6 i1#21
		i1#6 i1#24
	112(1) - 83(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
	112(1) - 98(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
	135(1) - 83(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
	135(1) - 98(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
	135(1) - 56(1) s1:
		s1#3 s1#7
		s1#3 s1#10
		s1#3 s1#13
		s1#4 s1#7
		s1#4 s1#10
		s1#4 s1#13
	135(1) - 71(1) s1:
		s1#3 s1#16
		s1#3 s1#19
		s1#3 s1#22
		s1#4 s1#16
		s1#4 s1#19
		s1#4 s1#22
	135(1) - 101(1) s2:
		s2#3 s2#16
		s2#3 s2#19
		s2#3 s2#22
		s2#4 s2#16
		s2#4 s2#19
		s2#4 s2#22
	135(1) - 86(1) s2:
		s2#3 s2#7
		s2#3 s2#10
		s2#3 s2#13
		s2#4 s2#7
		s2#4 s2#10
		s2#4 s2#13
Runtime Symex: 1.5306s
Adding SC constraints
Shared __CPROVER_threads_exited: 8R/5W
Shared __CPROVER_next_thread_id: 7R/5W
Shared x: 12R/2W
Shared i1: 10R/8W
Shared i2: 8R/8W
Shared t11: 3R/5W
Shared t21: 3R/5W
Shared t12: 3R/5W
Shared t22: 3R/5W
Shared s1: 8R/8W
Shared s2: 8R/8W
Shared n: 14R/2W
Shared main::1::t1!0@1: 2R/2W
Shared main::1::t2!0@1: 2R/2W
Shared main::1::t3!0@1: 2R/2W
Shared main::1::t4!0@1: 2R/2W
Shared symex_dynamic::dynamic_object1: 12R/4W
size of program expression: 1935 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0147945s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0209686s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.130556s
Solving with Deagle's Closure solver
214318 variables, 905674 clauses
ClosureSolver finishes with 278 conflicts, 739 decisions, and 135903 propagations. 1612 theory propagations and 6 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.175888s
Runtime decision procedure: 0.219811s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-1.wvr.c function main
[nodatarace.assertion.0] line 130 No data races on variable i1 between line 111 and line 53: SUCCESS
[nodatarace.assertion.1] line 130 No data races on variable i1 between line 111 and line 68: SUCCESS
[nodatarace.assertion.2] line 130 No data races on variable i1 between line 135 and line 53: SUCCESS
[nodatarace.assertion.3] line 130 No data races on variable i1 between line 135 and line 68: SUCCESS
[nodatarace.assertion.4] line 130 No data races on variable i2 between line 112 and line 83: SUCCESS
[nodatarace.assertion.5] line 130 No data races on variable i2 between line 112 and line 98: SUCCESS
[nodatarace.assertion.6] line 130 No data races on variable i2 between line 135 and line 83: SUCCESS
[nodatarace.assertion.7] line 130 No data races on variable i2 between line 135 and line 98: SUCCESS
[nodatarace.assertion.8] line 130 No data races on variable s1 between line 135 and line 56: SUCCESS
[nodatarace.assertion.9] line 130 No data races on variable s1 between line 135 and line 71: SUCCESS
[nodatarace.assertion.10] line 130 No data races on variable s2 between line 135 and line 101: SUCCESS
[nodatarace.assertion.11] line 130 No data races on variable s2 between line 135 and line 86: SUCCESS

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