./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-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-misc-1.wvr.c
Converting
Type-checking parallel-misc-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-misc-1.wvr file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-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 2 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
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
Unwinding loop create_fresh_int_array.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c line 113 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-misc-1.wvr.c line 113 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-misc-1.wvr.c line 113 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
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-misc-1.wvr.c line 46 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
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-misc-1.wvr.c line 46 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
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-misc-1.wvr.c line 46 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 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 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-misc-1.wvr.c line 63 function thread2 thread 2
aborting path on assume(fals[Warning][Unknown] Invalidating expressions: AddrOf(Var(bag1,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:83:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(bag2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:84:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(cap1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:85:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(cap2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:86:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(sum1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:87:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(sum2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:88:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(i, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:89:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(j, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:90:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(N, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:91:3)
[Warning][Unknown] Invalidating expressions: IndexPI(Lval(Var(arr, NoOffset)), Lval(Var(i___0, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:114:5)
[Warning][Race] Memory location sum2@parallel-misc-1.wvr.c:40:35 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:99:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:69:7)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:99:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:75:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:102:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:99:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:69:7)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:99:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:75:3)
[Warning][Race] Memory location sum1@parallel-misc-1.wvr.c:40:29 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:98:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:52:7)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:98:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:58:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:102:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:98:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:52:7)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:98:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c:58:3)

Summary for all memory locations:
	safe:            9
	vulnerable:      0
	unsafe:          2
	-------------------
	total:          11
e) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 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-misc-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
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-misc-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
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-misc-1.wvr.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 102 103 52 53 58 59 69 70 75 76 83 84 
The number of races before goblint filter: 568
The number of races after goblint filter: 46
Race categories: 10
	83(1) - 52(1) bag1:
		bag1#2 bag1#8
		bag1#2 bag1#9
		bag1#2 bag1#10
		bag1#2 bag1#17
		bag1#2 bag1#18
		bag1#2 bag1#19
		bag1#2 bag1#26
		bag1#2 bag1#27
		bag1#2 bag1#28
	83(1) - 53(1) bag1:
		bag1#2 bag1#11
		bag1#2 bag1#20
		bag1#2 bag1#29
	83(1) - 58(1) bag1:
		bag1#2 bag1#30
		bag1#2 bag1#31
		bag1#2 bag1#32
	84(1) - 69(1) bag2:
		bag2#2 bag2#8
		bag2#2 bag2#9
		bag2#2 bag2#10
		bag2#2 bag2#17
		bag2#2 bag2#18
		bag2#2 bag2#19
		bag2#2 bag2#26
		bag2#2 bag2#27
		bag2#2 bag2#28
	84(1) - 70(1) bag2:
		bag2#2 bag2#11
		bag2#2 bag2#20
		bag2#2 bag2#29
	84(1) - 75(1) bag2:
		bag2#2 bag2#30
		bag2#2 bag2#31
		bag2#2 bag2#32
	102(1) - 52(1) sum1:
		sum1#3 sum1#7
		sum1#3 sum1#10
		sum1#3 sum1#13
		sum1#4 sum1#7
		sum1#4 sum1#10
		sum1#4 sum1#13
	102(1) - 58(1) sum1:
		sum1#3 sum1#16
		sum1#4 sum1#16
	102(1) - 69(1) sum2:
		sum2#3 sum2#7
		sum2#3 sum2#10
		sum2#3 sum2#13
		sum2#4 sum2#7
		sum2#4 sum2#10
		sum2#4 sum2#13
	102(1) - 75(1) sum2:
		sum2#3 sum2#16
		sum2#4 sum2#16
Runtime Symex: 2.7541s
Adding SC constraints
Shared __CPROVER_threads_exited: 4R/3W
Shared __CPROVER_next_thread_id: 3R/3W
Shared A: 18R/2W
Shared bag1: 24R/8W
Shared bag2: 24R/8W
Shared cap1: 3R/2W
Shared cap2: 3R/2W
Shared sum1: 10R/6W
Shared sum2: 10R/6W
Shared i: 36R/5W
Shared j: 36R/5W
Shared N: 6R/2W
Shared main::1::t1!0@1: 2R/2W
Shared main::1::t2!0@1: 2R/2W
Shared symex_dynamic::dynamic_object1: 42R/4W
size of program expression: 2232 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.042323s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.030997s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.923789s
Solving with Deagle's Closure solver
1277762 variables, 5849266 clauses
ClosureSolver finishes with 300 conflicts, 1165548 decisions, and 3594906 propagations. 524 theory propagations and 4 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 1.66768s
Runtime decision procedure: 1.73464s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-1.wvr.c function main
[nodatarace.assertion.0] line 99 No data races on variable bag1 between line 83 and line 52: SUCCESS
[nodatarace.assertion.1] line 99 No data races on variable bag1 between line 83 and line 53: SUCCESS
[nodatarace.assertion.2] line 99 No data races on variable bag1 between line 83 and line 58: SUCCESS
[nodatarace.assertion.3] line 99 No data races on variable bag2 between line 84 and line 69: SUCCESS
[nodatarace.assertion.4] line 99 No data races on variable bag2 between line 84 and line 70: SUCCESS
[nodatarace.assertion.5] line 99 No data races on variable bag2 between line 84 and line 75: SUCCESS
[nodatarace.assertion.6] line 99 No data races on variable sum1 between line 102 and line 52: SUCCESS
[nodatarace.assertion.7] line 99 No data races on variable sum1 between line 102 and line 58: SUCCESS
[nodatarace.assertion.8] line 99 No data races on variable sum2 between line 102 and line 69: SUCCESS
[nodatarace.assertion.9] line 99 No data races on variable sum2 between line 102 and line 75: SUCCESS

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