./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.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/unroll-cond-5.wvr.c
Converting
Type-checking unroll-cond-5.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 unroll-cond-5.wvr file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.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
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:103:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:103:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n,
                                     NoOffset)), AddrOf(Var(size, NoOffset)), AddrOf(Var(x2, NoOffset)), AddrOf(Var(x1, NoOffset)), AddrOf(Var(f, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:103:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(n, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:103:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(size, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:104:3)
[Warning][Unknown] Invalidating expressions: IndexPI(Lval(Var(arr, NoOffset)), Lval(Var(i, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:126:5)
[Warning][Race] Memory location x1@unroll-cond-5.wvr.c:42:5 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:110:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:50:5)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:110:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:51:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:114:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:110:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:51:5)
[Warning][Race] Memory location x2@unroll-cond-5.wvr.c:42:9 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:60:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:61:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:63:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:64:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:66:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:67:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:69:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:70:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:72:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:73:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:77:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:78:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:82:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:83:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:87:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:88:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:92:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:93:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:114:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:61:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:64:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:67:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:70:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:73:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:78:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:83:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:88:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:111:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c:93:5)

Summary for all memory locations:
	safe:            4
	vulnerable:      0
	unsafe:          2
	-------------------
	total:           6
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
Unwinding loop create_fresh_int_array.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c line 125 function create_fresh_int_array thread 0
Not unwinding loop create_fresh_int_array.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c line 125 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 1
Unwinding loop thread1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c line 49 function thread1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Not unwinding loop thread1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c line 49 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
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/unroll-cond-5.wvr.c line 59 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
Not unwinding loop thread2.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c line 59 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
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/unroll-cond-5.wvr.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 103 104 114 115 50 51 52 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 77 78 79 82 83 84 87 88 89 92 93 94 
The number of races before goblint filter: 304
The number of races after goblint filter: 64
Race categories: 20
	104(1) - 50(1) size:
		size#2 size#3
		size#2 size#4
		size#2 size#5
		size#2 size#6
	104(1) - 60(1) size:
		size#2 size#7
		size#2 size#8
		size#2 size#17
		size#2 size#18
	104(1) - 63(1) size:
		size#2 size#9
		size#2 size#10
		size#2 size#19
		size#2 size#20
	104(1) - 66(1) size:
		size#2 size#11
		size#2 size#12
		size#2 size#21
		size#2 size#22
	104(1) - 69(1) size:
		size#2 size#13
		size#2 size#14
		size#2 size#23
		size#2 size#24
	104(1) - 72(1) size:
		size#2 size#15
		size#2 size#16
		size#2 size#25
		size#2 size#26
	104(1) - 77(1) size:
		size#2 size#27
		size#2 size#28
	104(1) - 82(1) size:
		size#2 size#29
		size#2 size#30
	104(1) - 87(1) size:
		size#2 size#31
		size#2 size#32
	104(1) - 92(1) size:
		size#2 size#33
		size#2 size#34
	114(1) - 51(1) x1:
		x1#2 x1#10
		x1#2 x1#17
		x1#3 x1#10
		x1#3 x1#17
	114(1) - 61(1) x2:
		x2#2 x2#10
		x2#2 x2#45
		x2#3 x2#10
		x2#3 x2#45
	114(1) - 64(1) x2:
		x2#2 x2#17
		x2#2 x2#52
		x2#3 x2#17
		x2#3 x2#52
	114(1) - 67(1) x2:
		x2#2 x2#24
		x2#2 x2#59
		x2#3 x2#24
		x2#3 x2#59
	114(1) - 70(1) x2:
		x2#2 x2#31
		x2#2 x2#66
		x2#3 x2#31
		x2#3 x2#66
	114(1) - 73(1) x2:
		x2#2 x2#38
		x2#2 x2#73
		x2#3 x2#38
		x2#3 x2#73
	114(1) - 78(1) x2:
		x2#2 x2#80
		x2#3 x2#80
	114(1) - 83(1) x2:
		x2#2 x2#87
		x2#3 x2#87
	114(1) - 88(1) x2:
		x2#2 x2#94
		x2#3 x2#94
	114(1) - 93(1) x2:
		x2#2 x2#101
		x2#3 x2#101
Runtime Symex: 1.50219s
Adding SC constraints
Shared size: 32R/2W
Shared f: 16R/2W
Shared __CPROVER_threads_exited: 4R/3W
Shared __CPROVER_next_thread_id: 3R/3W
Shared x1: 14R/3W
Shared x2: 86R/15W
Shared n: 8R/2W
Shared main::1::t1!0@1: 2R/2W
Shared main::1::t2!0@1: 2R/2W
Shared symex_dynamic::dynamic_object1: 16R/3W
size of program expression: 1846 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0369306s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0251245s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.132282s
Solving with Deagle's Closure solver
209976 variables, 916000 clauses
ClosureSolver finishes with 25 conflicts, 125 decisions, and 52641 propagations. 526 theory propagations and 2 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.150275s
Runtime decision procedure: 0.205417s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/unroll-cond-5.wvr.c function main
[nodatarace.assertion.0] line 111 No data races on variable size between line 104 and line 50: SUCCESS
[nodatarace.assertion.1] line 111 No data races on variable size between line 104 and line 60: SUCCESS
[nodatarace.assertion.2] line 111 No data races on variable size between line 104 and line 63: SUCCESS
[nodatarace.assertion.3] line 111 No data races on variable size between line 104 and line 66: SUCCESS
[nodatarace.assertion.4] line 111 No data races on variable size between line 104 and line 69: SUCCESS
[nodatarace.assertion.5] line 111 No data races on variable size between line 104 and line 72: SUCCESS
[nodatarace.assertion.6] line 111 No data races on variable size between line 104 and line 77: SUCCESS
[nodatarace.assertion.7] line 111 No data races on variable size between line 104 and line 82: SUCCESS
[nodatarace.assertion.8] line 111 No data races on variable size between line 104 and line 87: SUCCESS
[nodatarace.assertion.9] line 111 No data races on variable size between line 104 and line 92: SUCCESS
[nodatarace.assertion.10] line 111 No data races on variable x1 between line 114 and line 51: SUCCESS
[nodatarace.assertion.11] line 111 No data races on variable x2 between line 114 and line 61: SUCCESS
[nodatarace.assertion.12] line 111 No data races on variable x2 between line 114 and line 64: SUCCESS
[nodatarace.assertion.13] line 111 No data races on variable x2 between line 114 and line 67: SUCCESS
[nodatarace.assertion.14] line 111 No data races on variable x2 between line 114 and line 70: SUCCESS
[nodatarace.assertion.15] line 111 No data races on variable x2 between line 114 and line 73: SUCCESS
[nodatarace.assertion.16] line 111 No data races on variable x2 between line 114 and line 78: SUCCESS
[nodatarace.assertion.17] line 111 No data races on variable x2 between line 114 and line 83: SUCCESS
[nodatarace.assertion.18] line 111 No data races on variable x2 between line 114 and line 88: SUCCESS
[nodatarace.assertion.19] line 111 No data races on variable x2 between line 114 and line 93: SUCCESS

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