./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i


--------------------------------------------------------------------------------


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/pthread-lit/fk2012.i
Converting
Type-checking fk2012
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 fk2012 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i line 720
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] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1066:2)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1028:5)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:179:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:184:1)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:189:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:194:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:199:1)
[Warning][Race] Memory location counter@fk2012.i:1002:14 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1031:5)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1032:2)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1040:6)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1043:2)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1051:2)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1054:5)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1055:5)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1032:2)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1038:2)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1040:6)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1054:5)
[Warning][Race] Memory location lock2@fk2012.i:1001:14 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1017:5)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1023:5)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1018:5)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1024:5)
[Warning][Race] Memory location lock1@fk2012.i:1000:14 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1005:5)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1011:5)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1006:5)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1012:5)

Summary for all memory locations:
	safe:            0
	vulnerable:      0
	unsafe:          3
	-------------------
	total:           3
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
Unwinding loop main.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i line 1065 function main thread 0
Not unwinding loop main.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i line 1065 function main 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
Unwinding loop producer.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i line 1039 function producer thread 1
Not unwinding loop producer.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i line 1039 function producer 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
Unwinding loop consumer.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i line 1049 function consumer 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 consumer.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i line 1049 function consumer 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 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
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Unwinding loop producer.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i line 1039 function producer thread 3
Not unwinding loop producer.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i line 1039 function producer 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 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
Unwinding loop consumer.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i line 1049 function consumer 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 consumer.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i line 1049 function consumer 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
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/pthread-lit/fk2012.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 1005 1006 1007 1011 1012 1013 1017 1018 1019 1023 1024 1025 1028 1029 1031 1032 1033 1038 1039 1040 1041 1043 1044 1051 1052 1054 1055 1056 1066 1067 
The number of races before goblint filter: 331
The number of races after goblint filter: 183
Race categories: 48
	1031(1) - 1032(1) counter:
		counter#3 counter#20
	1031(1) - 1038(1) counter:
		counter#3 counter#21
	1031(1) - 1040(1) counter:
		counter#3 counter#23
		counter#3 counter#25
	1031(1) - 1054(1) counter:
		counter#3 counter#15
		counter#3 counter#30
		counter#18 counter#30
	1032(1) - 1031(1) counter:
		counter#5 counter#18
	1032(1) - 1032(1) counter:
		counter#4 counter#20
		counter#5 counter#19
		counter#5 counter#20
	1032(1) - 1038(1) counter:
		counter#4 counter#21
		counter#5 counter#21
	1032(1) - 1040(1) counter:
		counter#4 counter#23
		counter#4 counter#25
		counter#5 counter#22
		counter#5 counter#23
		counter#5 counter#24
		counter#5 counter#25
	1032(1) - 1043(1) counter:
		counter#5 counter#26
	1032(1) - 1051(1) counter:
		counter#5 counter#12
		counter#5 counter#13
		counter#5 counter#27
		counter#5 counter#28
		counter#20 counter#27
		counter#20 counter#28
	1032(1) - 1054(1) counter:
		counter#4 counter#15
		counter#5 counter#14
		counter#5 counter#15
		counter#4 counter#30
		counter#5 counter#29
		counter#5 counter#30
		counter#19 counter#30
		counter#20 counter#29
		counter#20 counter#30
	1032(1) - 1055(1) counter:
		counter#5 counter#16
		counter#5 counter#17
		counter#5 counter#31
		counter#5 counter#32
		counter#20 counter#31
		counter#20 counter#32
	1038(1) - 1031(1) counter:
		counter#6 counter#18
	1038(1) - 1032(1) counter:
		counter#6 counter#19
		counter#6 counter#20
	1038(1) - 1038(1) counter:
		counter#6 counter#21
	1038(1) - 1040(1) counter:
		counter#6 counter#22
		counter#6 counter#23
		counter#6 counter#24
		counter#6 counter#25
	1038(1) - 1043(1) counter:
		counter#6 counter#26
	1038(1) - 1051(1) counter:
		counter#6 counter#12
		counter#6 counter#13
		counter#6 counter#27
		counter#6 counter#28
		counter#21 counter#27
		counter#21 counter#28
	1038(1) - 1054(1) counter:
		counter#6 counter#14
		counter#6 counter#15
		counter#6 counter#29
		counter#6 counter#30
		counter#21 counter#29
		counter#21 counter#30
	1038(1) - 1055(1) counter:
		counter#6 counter#16
		counter#6 counter#17
		counter#6 counter#31
		counter#6 counter#32
		counter#21 counter#31
		counter#21 counter#32
	1040(1) - 1031(1) counter:
		counter#8 counter#18
		counter#10 counter#18
	1040(1) - 1032(1) counter:
		counter#7 counter#20
		counter#8 counter#19
		counter#8 counter#20
		counter#9 counter#20
		counter#10 counter#19
		counter#10 counter#20
	1040(1) - 1038(1) counter:
		counter#7 counter#21
		counter#8 counter#21
		counter#9 counter#21
		counter#10 counter#21
	1040(1) - 1040(1) counter:
		counter#7 counter#23
		counter#7 counter#25
		counter#8 counter#22
		counter#8 counter#23
		counter#8 counter#24
		counter#8 counter#25
		counter#9 counter#23
		counter#9 counter#25
		counter#10 counter#22
		counter#10 counter#23
		counter#10 counter#24
		counter#10 counter#25
	1040(1) - 1043(1) counter:
		counter#8 counter#26
		counter#10 counter#26
	1040(1) - 1051(1) counter:
		counter#8 counter#12
		counter#8 counter#13
		counter#10 counter#12
		counter#10 counter#13
		counter#8 counter#27
		counter#8 counter#28
		counter#10 counter#27
		counter#10 counter#28
		counter#23 counter#27
		counter#23 counter#28
		counter#25 counter#27
		counter#25 counter#28
	1040(1) - 1054(1) counter:
		counter#7 counter#15
		counter#8 counter#14
		counter#8 counter#15
		counter#9 counter#15
		counter#10 counter#14
		counter#10 counter#15
		counter#7 counter#30
		counter#8 counter#29
		counter#8 counter#30
		counter#9 counter#30
		counter#10 counter#29
		counter#10 counter#30
		counter#22 counter#30
		counter#23 counter#29
		counter#23 counter#30
		counter#24 counter#30
		counter#25 counter#29
		counter#25 counter#30
	1040(1) - 1055(1) counter:
		counter#8 counter#16
		counter#8 counter#17
		counter#10 counter#16
		counter#10 counter#17
		counter#8 counter#31
		counter#8 counter#32
		counter#10 counter#31
		counter#10 counter#32
		counter#23 counter#31
		counter#23 counter#32
		counter#25 counter#31
		counter#25 counter#32
	1043(1) - 1032(1) counter:
		counter#11 counter#20
	1043(1) - 1038(1) counter:
		counter#11 counter#21
	1043(1) - 1040(1) counter:
		counter#11 counter#23
		counter#11 counter#25
	1043(1) - 1054(1) counter:
		counter#11 counter#15
		counter#11 counter#30
		counter#26 counter#30
	1051(1) - 1032(1) counter:
		counter#12 counter#20
		counter#13 counter#20
	1051(1) - 1038(1) counter:
		counter#12 counter#21
		counter#13 counter#21
	1051(1) - 1040(1) counter:
		counter#12 counter#23
		counter#12 counter#25
		counter#13 counter#23
		counter#13 counter#25
	1051(1) - 1054(1) counter:
		counter#12 counter#30
		counter#13 counter#30
	1054(1) - 1031(1) counter:
		counter#15 counter#18
	1054(1) - 1032(1) counter:
		counter#14 counter#20
		counter#15 counter#19
		counter#15 counter#20
	1054(1) - 1038(1) counter:
		counter#14 counter#21
		counter#15 counter#21
	1054(1) - 1040(1) counter:
		counter#14 counter#23
		counter#14 counter#25
		counter#15 counter#22
		counter#15 counter#23
		counter#15 counter#24
		counter#15 counter#25
	1054(1) - 1043(1) counter:
		counter#15 counter#26
	1054(1) - 1051(1) counter:
		counter#15 counter#27
		counter#15 counter#28
	1054(1) - 1054(1) counter:
		counter#14 counter#30
		counter#15 counter#29
		counter#15 counter#30
	1054(1) - 1055(1) counter:
		counter#15 counter#31
		counter#15 counter#32
	1055(1) - 1032(1) counter:
		counter#16 counter#20
		counter#17 counter#20
	1055(1) - 1038(1) counter:
		counter#16 counter#21
		counter#17 counter#21
	1055(1) - 1040(1) counter:
		counter#16 counter#23
		counter#16 counter#25
		counter#17 counter#23
		counter#17 counter#25
	1055(1) - 1054(1) counter:
		counter#16 counter#30
		counter#17 counter#30
Runtime Symex: 0.703047s
Adding SC constraints
Shared __CPROVER_threads_exited: 4R/5W
Shared __CPROVER_next_thread_id: 3R/5W
Shared lock1: 16R/18W
Shared lock2: 6R/8W
Shared counter: 20R/12W
size of program expression: 1598 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0162412s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0127593s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.00125394s
Solving with Deagle's Closure solver
10826 variables, 40519 clauses
ClosureSolver finishes with 124 conflicts, 20821 decisions, and 63640 propagations. 117 theory propagations and 3 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00904961s
Runtime decision procedure: 0.0354304s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38661 clauses
ClosureSolver finishes with 124 conflicts, 22729 decisions, and 72817 propagations. 117 theory propagations and 3 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00111955s
Runtime decision procedure: 0.0011588s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38662 clauses
ClosureSolver finishes with 127 conflicts, 24641 decisions, and 82967 propagations. 122 theory propagations and 3 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00137367s
Runtime decision procedure: 0.0014076s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38663 clauses
ClosureSolver finishes with 193 conflicts, 38092 decisions, and 173299 propagations. 237 theory propagations and 18 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00967504s
Runtime decision procedure: 0.00972019s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38664 clauses
ClosureSolver finishes with 194 conflicts, 40108 decisions, and 182861 propagations. 237 theory propagations and 18 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0015653s
Runtime decision procedure: 0.00160625s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38652 clauses
ClosureSolver finishes with 243 conflicts, 43055 decisions, and 206715 propagations. 424 theory propagations and 28 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00328552s
Runtime decision procedure: 0.00331967s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38653 clauses
ClosureSolver finishes with 271 conflicts, 48983 decisions, and 250469 propagations. 431 theory propagations and 28 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00463692s
Runtime decision procedure: 0.00468527s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38654 clauses
ClosureSolver finishes with 271 conflicts, 50682 decisions, and 259641 propagations. 431 theory propagations and 28 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00151117s
Runtime decision procedure: 0.00155021s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38655 clauses
ClosureSolver finishes with 271 conflicts, 52421 decisions, and 268813 propagations. 431 theory propagations and 28 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00115623s
Runtime decision procedure: 0.00118734s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38656 clauses
ClosureSolver finishes with 327 conflicts, 54760 decisions, and 295198 propagations. 593 theory propagations and 46 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00449543s
Runtime decision procedure: 0.00452772s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38657 clauses
ClosureSolver finishes with 339 conflicts, 57596 decisions, and 314179 propagations. 644 theory propagations and 48 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00270308s
Runtime decision procedure: 0.00273487s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38640 clauses
ClosureSolver finishes with 346 conflicts, 59465 decisions, and 325246 propagations. 647 theory propagations and 51 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00153154s
Runtime decision procedure: 0.00157269s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38641 clauses
ClosureSolver finishes with 346 conflicts, 61286 decisions, and 334413 propagations. 647 theory propagations and 51 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00119905s
Runtime decision procedure: 0.0012282s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38642 clauses
ClosureSolver finishes with 346 conflicts, 63098 decisions, and 343580 propagations. 647 theory propagations and 51 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00117773s
Runtime decision procedure: 0.00121639s
Running propositional reduction
Solving with Deagle's Closure solver
10826 variables, 38643 clauses
ClosureSolver finishes with 419 conflicts, 63342 decisions, and 365049 propagations. 913 theory propagations and 69 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.00406423s
Runtime decision procedure: 0.00408193s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i function main
[nodatarace.assertion.0] line 1071 No data races on variable counter between line 1031 and line 1032: SUCCESS
[nodatarace.assertion.1] line 1071 No data races on variable counter between line 1031 and line 1038: SUCCESS
[nodatarace.assertion.2] line 1071 No data races on variable counter between line 1031 and line 1040: SUCCESS
[nodatarace.assertion.3] line 1071 No data races on variable counter between line 1031 and line 1054: SUCCESS
[nodatarace.assertion.4] line 1071 No data races on variable counter between line 1032 and line 1031: SUCCESS
[nodatarace.assertion.5] line 1071 No data races on variable counter between line 1032 and line 1032: SUCCESS
[nodatarace.assertion.6] line 1071 No data races on variable counter between line 1032 and line 1038: SUCCESS
[nodatarace.assertion.7] line 1071 No data races on variable counter between line 1032 and line 1040: SUCCESS
[nodatarace.assertion.8] line 1071 No data races on variable counter between line 1032 and line 1043: SUCCESS
[nodatarace.assertion.9] line 1071 No data races on variable counter between line 1032 and line 1051: SUCCESS
[nodatarace.assertion.10] line 1071 No data races on variable counter between line 1032 and line 1054: SUCCESS
[nodatarace.assertion.11] line 1071 No data races on variable counter between line 1032 and line 1055: SUCCESS
[nodatarace.assertion.12] line 1071 No data races on variable counter between line 1038 and line 1031: SUCCESS
[nodatarace.assertion.13] line 1071 No data races on variable counter between line 1038 and line 1032: SUCCESS
[nodatarace.assertion.14] line 1071 No data races on variable counter between line 1038 and line 1038: SUCCESS
[nodatarace.assertion.15] line 1071 No data races on variable counter between line 1038 and line 1040: SUCCESS
[nodatarace.assertion.16] line 1071 No data races on variable counter between line 1038 and line 1043: SUCCESS
[nodatarace.assertion.17] line 1071 No data races on variable counter between line 1038 and line 1051: FAILURE
[nodatarace.assertion.18] line 1071 No data races on variable counter between line 1038 and line 1054: FAILURE
[nodatarace.assertion.19] line 1071 No data races on variable counter between line 1038 and line 1055: FAILURE
[nodatarace.assertion.20] line 1071 No data races on variable counter between line 1040 and line 1031: SUCCESS
[nodatarace.assertion.21] line 1071 No data races on variable counter between line 1040 and line 1032: SUCCESS
[nodatarace.assertion.22] line 1071 No data races on variable counter between line 1040 and line 1038: SUCCESS
[nodatarace.assertion.23] line 1071 No data races on variable counter between line 1040 and line 1040: SUCCESS
[nodatarace.assertion.24] line 1071 No data races on variable counter between line 1040 and line 1043: SUCCESS
[nodatarace.assertion.25] line 1071 No data races on variable counter between line 1040 and line 1051: FAILURE
[nodatarace.assertion.26] line 1071 No data races on variable counter between line 1040 and line 1054: FAILURE
[nodatarace.assertion.27] line 1071 No data races on variable counter between line 1040 and line 1055: FAILURE
[nodatarace.assertion.28] line 1071 No data races on variable counter between line 1043 and line 1032: SUCCESS
[nodatarace.assertion.29] line 1071 No data races on variable counter between line 1043 and line 1038: SUCCESS
[nodatarace.assertion.30] line 1071 No data races on variable counter between line 1043 and line 1040: SUCCESS
[nodatarace.assertion.31] line 1071 No data races on variable counter between line 1043 and line 1054: FAILURE
[nodatarace.assertion.32] line 1071 No data races on variable counter between line 1051 and line 1032: SUCCESS
[nodatarace.assertion.33] line 1071 No data races on variable counter between line 1051 and line 1038: FAILURE
[nodatarace.assertion.34] line 1071 No data races on variable counter between line 1051 and line 1040: FAILURE
[nodatarace.assertion.35] line 1071 No data races on variable counter between line 1051 and line 1054: SUCCESS
[nodatarace.assertion.36] line 1071 No data races on variable counter between line 1054 and line 1031: SUCCESS
[nodatarace.assertion.37] line 1071 No data races on variable counter between line 1054 and line 1032: SUCCESS
[nodatarace.assertion.38] line 1071 No data races on variable counter between line 1054 and line 1038: FAILURE
[nodatarace.assertion.39] line 1071 No data races on variable counter between line 1054 and line 1040: FAILURE
[nodatarace.assertion.40] line 1071 No data races on variable counter between line 1054 and line 1043: FAILURE
[nodatarace.assertion.41] line 1071 No data races on variable counter between line 1054 and line 1051: SUCCESS
[nodatarace.assertion.42] line 1071 No data races on variable counter between line 1054 and line 1054: SUCCESS
[nodatarace.assertion.43] line 1071 No data races on variable counter between line 1054 and line 1055: SUCCESS
[nodatarace.assertion.44] line 1071 No data races on variable counter between line 1055 and line 1032: SUCCESS
[nodatarace.assertion.45] line 1071 No data races on variable counter between line 1055 and line 1038: FAILURE
[nodatarace.assertion.46] line 1071 No data races on variable counter between line 1055 and line 1040: FAILURE
[nodatarace.assertion.47] line 1071 No data races on variable counter between line 1055 and line 1054: SUCCESS

** 14 of 48 failed (15 iterations)
VERIFICATION FAILED
