./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.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/test-easy10.wvr.c
Converting
Type-checking test-easy10.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 test-easy10.wvr file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.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
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:136:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:136:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f22,
                                     NoOffset)), AddrOf(Var(f21, NoOffset)), AddrOf(Var(f12, NoOffset)), AddrOf(Var(f11, NoOffset)), AddrOf(Var(t22, NoOffset)), AddrOf(Var(t21, NoOffset)), AddrOf(Var(t12, NoOffset)), AddrOf(Var(t11, NoOffset)), AddrOf(Var(y2, NoOffset)), AddrOf(Var(y1, NoOffset)), AddrOf(Var(x2, NoOffset)), AddrOf(Var(x1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:136:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(x1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:136:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:137:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:137:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f22, NoOffset)), AddrOf(Var(f21, NoOffset)), AddrOf(Var(f12, NoOffset)), AddrOf(Var(f11, NoOffset)), AddrOf(Var(t22, NoOffset)), AddrOf(Var(t21, NoOffset)), AddrOf(Var(t12, NoOffset)), AddrOf(Var(t11, NoOffset)), AddrOf(Var(y2, NoOffset)), AddrOf(Var(y1, NoOffset)), AddrOf(Var(x2, NoOffset)), AddrOf(Var(x1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:137:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(x2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:137:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:138:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:138:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f22, NoOffset)), AddrOf(Var(f21, NoOffset)), AddrOf(Var(f12, NoOffset)), AddrOf(Var(f11, NoOffset)), AddrOf(Var(t22, NoOffset)), AddrOf(Var(t21, NoOffset)), AddrOf(Var(t12, NoOffset)), AddrOf(Var(t11, NoOffset)), AddrOf(Var(y2, NoOffset)), AddrOf(Var(y1, NoOffset)), AddrOf(Var(x2, NoOffset)), AddrOf(Var(x1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:138:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(y1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:138:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:139:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:139:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f22, NoOffset)), AddrOf(Var(f21, NoOffset)), AddrOf(Var(f12, NoOffset)), AddrOf(Var(f11, NoOffset)), AddrOf(Var(t22, NoOffset)), AddrOf(Var(t21, NoOffset)), AddrOf(Var(t12, NoOffset)), AddrOf(Var(t11, NoOffset)), AddrOf(Var(y2, NoOffset)), AddrOf(Var(y1, NoOffset)), AddrOf(Var(x2, NoOffset)), AddrOf(Var(x1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:139:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(y2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:139:3)
[Warning][Race] Memory location f12@test-easy10.wvr.c:39:32 (race with conf. 110):
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:146:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:98:3)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:147:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:121:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:146:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:95:3)
[Warning][Race] Memory location f21@test-easy10.wvr.c:39:37 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:144:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:52:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:145:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:75:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:145:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:72:3)
[Warning][Race] Memory location f11@test-easy10.wvr.c:39:27 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:144:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:52:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:145:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:75:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:144:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:49:3)
[Warning][Race] Memory location f22@test-easy10.wvr.c:39:42 (race with conf. 110):
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:146:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:98:3)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:147:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:121:3)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:147:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:118:3)
[Warning][Race] Memory location y2@test-easy10.wvr.c:38:26 (race with conf. 110):
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:146:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:101:3)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:147:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:112:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:152:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:146:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:104:3)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:147:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:115:3)
[Warning][Race] Memory location x2@test-easy10.wvr.c:38:18 (race with conf. 110):
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:146:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:89:3)
  read with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:147:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:124:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:152:3)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:146:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:92:3)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:147:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:127:3)
[Warning][Race] Memory location y1@test-easy10.wvr.c:38:22 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:144:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:55:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:145:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:66:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:152:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:144:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:58:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:145:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:69:3)
[Warning][Race] Memory location x1@test-easy10.wvr.c:38:14 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:144:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:43:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:145:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:78:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:152:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:144:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:46:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:145:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:81:3)

Summary for all memory locations:
	safe:            4
	vulnerable:      0
	unsafe:          8
	-------------------
	total:          12
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 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 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort 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/test-easy10.wvr.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 101 102 104 105 112 113 115 116 118 119 121 122 124 125 127 128 136 137 152 153 43 44 46 47 49 50 52 53 55 56 58 59 66 67 69 70 72 73 75 76 78 79 81 82 89 90 92 93 95 96 98 99 
The number of races before goblint filter: 76
The number of races after goblint filter: 24
Race categories: 16
	136(1) - 44(1) x1:
		x1#2 x1#5
	136(1) - 47(1) x1:
		x1#2 x1#7
	136(1) - 79(1) x1:
		x1#2 x1#8
	136(1) - 82(1) x1:
		x1#2 x1#10
	152(1) - 47(1) x1:
		x1#3 x1#7
		x1#4 x1#7
	152(1) - 82(1) x1:
		x1#3 x1#10
		x1#4 x1#10
	137(1) - 125(1) x2:
		x2#2 x2#8
	137(1) - 128(1) x2:
		x2#2 x2#10
	137(1) - 90(1) x2:
		x2#2 x2#5
	137(1) - 93(1) x2:
		x2#2 x2#7
	152(1) - 128(1) x2:
		x2#3 x2#10
		x2#4 x2#10
	152(1) - 93(1) x2:
		x2#3 x2#7
		x2#4 x2#7
	152(1) - 59(1) y1:
		y1#3 y1#7
		y1#4 y1#7
	152(1) - 70(1) y1:
		y1#3 y1#10
		y1#4 y1#10
	152(1) - 105(1) y2:
		y2#3 y2#7
		y2#4 y2#7
	152(1) - 116(1) y2:
		y2#3 y2#10
		y2#4 y2#10
Runtime Symex: 0.584667s
Adding SC constraints
Shared __CPROVER_threads_exited: 8R/5W
Shared __CPROVER_next_thread_id: 7R/5W
Shared x1: 4R/4W
Shared x2: 4R/4W
Shared y1: 4R/4W
Shared y2: 4R/4W
Shared t11: 2R/3W
Shared t12: 2R/3W
Shared t21: 2R/3W
Shared t22: 2R/3W
Shared f11: 2R/2W
Shared f12: 2R/2W
Shared f21: 2R/2W
Shared f22: 2R/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
size of program expression: 834 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.00359854s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00411888s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.00444394s
Solving with Deagle's Closure solver
8359 variables, 23489 clauses
ClosureSolver finishes with 197 conflicts, 473 decisions, and 74528 propagations. 877 theory propagations and 10 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.027922s
Runtime decision procedure: 0.0452468s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c function main
[nodatarace.assertion.0] line 147 No data races on variable x1 between line 136 and line 44: SUCCESS
[nodatarace.assertion.1] line 147 No data races on variable x1 between line 136 and line 47: SUCCESS
[nodatarace.assertion.2] line 147 No data races on variable x1 between line 136 and line 79: SUCCESS
[nodatarace.assertion.3] line 147 No data races on variable x1 between line 136 and line 82: SUCCESS
[nodatarace.assertion.4] line 147 No data races on variable x1 between line 152 and line 47: SUCCESS
[nodatarace.assertion.5] line 147 No data races on variable x1 between line 152 and line 82: SUCCESS
[nodatarace.assertion.6] line 147 No data races on variable x2 between line 137 and line 125: SUCCESS
[nodatarace.assertion.7] line 147 No data races on variable x2 between line 137 and line 128: SUCCESS
[nodatarace.assertion.8] line 147 No data races on variable x2 between line 137 and line 90: SUCCESS
[nodatarace.assertion.9] line 147 No data races on variable x2 between line 137 and line 93: SUCCESS
[nodatarace.assertion.10] line 147 No data races on variable x2 between line 152 and line 128: SUCCESS
[nodatarace.assertion.11] line 147 No data races on variable x2 between line 152 and line 93: SUCCESS
[nodatarace.assertion.12] line 147 No data races on variable y1 between line 152 and line 59: SUCCESS
[nodatarace.assertion.13] line 147 No data races on variable y1 between line 152 and line 70: SUCCESS
[nodatarace.assertion.14] line 147 No data races on variable y2 between line 152 and line 105: SUCCESS
[nodatarace.assertion.15] line 147 No data races on variable y2 between line 152 and line 116: SUCCESS

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