./deagle /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i --32


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


./deagle_exe --svcomp --graphml-witness error-witness.graphml --no-assertions --datarace /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i
Deagle version 2.2 64-bit x86_64 linux
which contains:
CBMC version 5.67.0 (svcomp24-11-gfd1b965b5-dirty) 64-bit x86_64 linux
Parsing /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i
Converting
Type-checking value-barrier
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_mutex_lock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_lock"
old definition in module value-barrier file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 839
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_lock> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-pthread_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module value-barrier file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 726
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 *pthread_create$$thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
file <builtin-library-pthread_cond_wait> line 7: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_cond_wait"
old definition in module value-barrier file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 939
signed int (pthread_cond_t *, pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_wait> line 7
signed int (pthread_cond_t *cond, pthread_mutex_t *mutex)
file <builtin-library-pthread_mutex_unlock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_unlock"
old definition in module value-barrier file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 844
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_unlock> line 17
signed int (pthread_mutex_t *mutex)
Removal of function pointers and virtual functions
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 1 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
Use SV-COMP unwinding strategy: 5
Deagle's solver is set!!!!!!
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
Unwinding loop main.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1028 function main thread 0
Unwinding loop main.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1028 function main thread 0
Unwinding loop main.0 iteration 3 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1028 function main thread 0
Unwinding loop main.0 iteration 4 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1028 function main thread 0
Not unwinding loop main.0 iteration 5 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1028 function main thread 0
Unwinding loop main.1 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1036 function main thread 0
Unwinding loop main.1 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1036 function main thread 0
Unwinding loop main.1 iteration 3 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1036 function main thread 0
Unwinding loop main.1 iteration 4 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1036 function main thread 0
Not unwinding loop main.1 iteration 5 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1036 function main thread 0
pointer handling for concurrency is unsound
Unwinding loop thread.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 1
Unwinding loop thread.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 1
Unwinding loop thread.0 iteration 3 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 1
Unwinding loop thread.0 iteration 4 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 1
Not unwinding loop thread.0 iteration 5 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 1
Unwinding loop thread.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 2
Unwinding loop thread.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 2
Unwinding loop thread.0 iteration 3 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 2
Unwinding loop thread.0 iteration 4 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 2
Not unwinding loop thread.0 iteration 5 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 2
Unwinding loop thread.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 3
Unwinding loop thread.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 3
Unwinding loop thread.0 iteration 3 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 3
Unwinding loop thread.0 iteration 4 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 3
Not unwinding loop thread.0 iteration 5 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 3
Unwinding loop thread.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 4
Unwinding loop thread.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 4
Unwinding loop thread.0 iteration 3 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 4
Unwinding loop thread.0 iteration 4 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 4
Not unwinding loop thread.0 iteration 5 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 4
aborting path on assume(false) at file <builtin-library-__spawned_thread> line 34 function __spawned_thread thread 5
Unwinding loop thread.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 5
Unwinding loop thread.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 5
Unwinding loop thread.0 iteration 3 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 5
Unwinding loop thread.0 iteration 4 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 5
Not unwinding loop thread.0 iteration 5 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/value-barrier.i line 1018 function thread thread 5
Start removing dummy accesses: 1676 steps before removal
symex_dynamic::dynamic_object1#11 is dummy and removed
symex_dynamic::dynamic_object1#13 is dummy and removed
symex_dynamic::dynamic_object1#15 is dummy and removed
symex_dynamic::dynamic_object1#17 is dummy and removed
symex_dynamic::dynamic_object1#19 is dummy and removed
1671 steps after removal
Handling datarace with no aid
The number of races before filter: 230
The number of races after filter: 230
The number of race categories before filter: 7
The number of race categories after filter: 7
	1015(1) - 1021(1) data
	1031(1) - 1021(1) data
	1012(1) - 1018(1) ready
	1033(1) - 1018(1) ready
	1014(1) - 30(1) ready_cond
	1013(1) - 40(1) ready_mutex
	1013(1) - 42(1) ready_mutex
Races between line 1015 - line 1021:
	data#1 data#3
	data#1 data#4
	data#1 data#5
	data#1 data#6
	data#1 data#7
Races between line 1031 - line 1021:
	data#2 data#3
	data#2 data#4
	data#2 data#5
	data#2 data#6
	data#2 data#7
Races between line 1012 - line 1018:
	ready#1 ready#3
	ready#1 ready#4
	ready#1 ready#5
	ready#1 ready#6
	ready#1 ready#7
	ready#1 ready#8
	ready#1 ready#9
	ready#1 ready#10
	ready#1 ready#11
	ready#1 ready#12
	ready#1 ready#13
	ready#1 ready#14
	ready#1 ready#15
	ready#1 ready#16
	ready#1 ready#17
	ready#1 ready#18
	ready#1 ready#19
	ready#1 ready#20
	ready#1 ready#21
	ready#1 ready#22
	ready#1 ready#23
	ready#1 ready#24
	ready#1 ready#25
	ready#1 ready#26
	ready#1 ready#27
Races between line 1033 - line 1018:
	ready#2 ready#3
	ready#2 ready#4
	ready#2 ready#5
	ready#2 ready#6
	ready#2 ready#7
	ready#2 ready#8
	ready#2 ready#9
	ready#2 ready#10
	ready#2 ready#11
	ready#2 ready#12
	ready#2 ready#13
	ready#2 ready#14
	ready#2 ready#15
	ready#2 ready#16
	ready#2 ready#17
	ready#2 ready#18
	ready#2 ready#19
	ready#2 ready#20
	ready#2 ready#21
	ready#2 ready#22
	ready#2 ready#23
	ready#2 ready#24
	ready#2 ready#25
	ready#2 ready#26
	ready#2 ready#27
Races between line 1014 - line 30:
	ready_cond#1 ready_cond#5
	ready_cond#1 ready_cond#8
	ready_cond#1 ready_cond#9
	ready_cond#1 ready_cond#12
	ready_cond#1 ready_cond#13
	ready_cond#1 ready_cond#16
	ready_cond#1 ready_cond#17
	ready_cond#1 ready_cond#20
	ready_cond#1 ready_cond#21
	ready_cond#1 ready_cond#24
	ready_cond#1 ready_cond#25
	ready_cond#1 ready_cond#28
	ready_cond#1 ready_cond#29
	ready_cond#1 ready_cond#32
	ready_cond#1 ready_cond#33
	ready_cond#1 ready_cond#36
	ready_cond#1 ready_cond#37
	ready_cond#1 ready_cond#40
	ready_cond#1 ready_cond#41
	ready_cond#1 ready_cond#44
	ready_cond#1 ready_cond#45
	ready_cond#1 ready_cond#48
	ready_cond#1 ready_cond#49
	ready_cond#1 ready_cond#52
	ready_cond#1 ready_cond#53
	ready_cond#1 ready_cond#56
	ready_cond#1 ready_cond#57
	ready_cond#1 ready_cond#60
	ready_cond#1 ready_cond#61
	ready_cond#1 ready_cond#64
	ready_cond#1 ready_cond#65
	ready_cond#1 ready_cond#68
	ready_cond#1 ready_cond#69
	ready_cond#1 ready_cond#72
	ready_cond#1 ready_cond#73
	ready_cond#1 ready_cond#76
	ready_cond#1 ready_cond#77
	ready_cond#1 ready_cond#80
	ready_cond#1 ready_cond#81
	ready_cond#1 ready_cond#84
	ready_cond#1 ready_cond#85
	ready_cond#1 ready_cond#88
	ready_cond#1 ready_cond#89
	ready_cond#1 ready_cond#92
	ready_cond#1 ready_cond#93
	ready_cond#1 ready_cond#96
	ready_cond#1 ready_cond#97
	ready_cond#1 ready_cond#100
	ready_cond#1 ready_cond#101
	ready_cond#1 ready_cond#104
Races between line 1013 - line 40:
	ready_mutex#1 ready_mutex#8
	ready_mutex#1 ready_mutex#10
	ready_mutex#1 ready_mutex#14
	ready_mutex#1 ready_mutex#16
	ready_mutex#1 ready_mutex#20
	ready_mutex#1 ready_mutex#22
	ready_mutex#1 ready_mutex#26
	ready_mutex#1 ready_mutex#28
	ready_mutex#1 ready_mutex#32
	ready_mutex#1 ready_mutex#34
	ready_mutex#1 ready_mutex#38
	ready_mutex#1 ready_mutex#40
	ready_mutex#1 ready_mutex#44
	ready_mutex#1 ready_mutex#46
	ready_mutex#1 ready_mutex#50
	ready_mutex#1 ready_mutex#52
	ready_mutex#1 ready_mutex#56
	ready_mutex#1 ready_mutex#58
	ready_mutex#1 ready_mutex#62
	ready_mutex#1 ready_mutex#64
	ready_mutex#1 ready_mutex#68
	ready_mutex#1 ready_mutex#70
	ready_mutex#1 ready_mutex#74
	ready_mutex#1 ready_mutex#76
	ready_mutex#1 ready_mutex#80
	ready_mutex#1 ready_mutex#82
	ready_mutex#1 ready_mutex#86
	ready_mutex#1 ready_mutex#88
	ready_mutex#1 ready_mutex#92
	ready_mutex#1 ready_mutex#94
	ready_mutex#1 ready_mutex#98
	ready_mutex#1 ready_mutex#100
	ready_mutex#1 ready_mutex#104
	ready_mutex#1 ready_mutex#106
	ready_mutex#1 ready_mutex#110
	ready_mutex#1 ready_mutex#112
	ready_mutex#1 ready_mutex#116
	ready_mutex#1 ready_mutex#118
	ready_mutex#1 ready_mutex#122
	ready_mutex#1 ready_mutex#124
	ready_mutex#1 ready_mutex#128
	ready_mutex#1 ready_mutex#130
	ready_mutex#1 ready_mutex#134
	ready_mutex#1 ready_mutex#136
	ready_mutex#1 ready_mutex#140
	ready_mutex#1 ready_mutex#142
	ready_mutex#1 ready_mutex#146
	ready_mutex#1 ready_mutex#148
	ready_mutex#1 ready_mutex#152
	ready_mutex#1 ready_mutex#154
	ready_mutex#1 ready_mutex#158
	ready_mutex#1 ready_mutex#160
	ready_mutex#1 ready_mutex#164
	ready_mutex#1 ready_mutex#166
	ready_mutex#1 ready_mutex#170
	ready_mutex#1 ready_mutex#172
	ready_mutex#1 ready_mutex#176
	ready_mutex#1 ready_mutex#178
	ready_mutex#1 ready_mutex#182
	ready_mutex#1 ready_mutex#184
Races between line 1013 - line 42:
	ready_mutex#1 ready_mutex#11
	ready_mutex#1 ready_mutex#13
	ready_mutex#1 ready_mutex#17
	ready_mutex#1 ready_mutex#19
	ready_mutex#1 ready_mutex#23
	ready_mutex#1 ready_mutex#25
	ready_mutex#1 ready_mutex#29
	ready_mutex#1 ready_mutex#31
	ready_mutex#1 ready_mutex#35
	ready_mutex#1 ready_mutex#37
	ready_mutex#1 ready_mutex#41
	ready_mutex#1 ready_mutex#43
	ready_mutex#1 ready_mutex#47
	ready_mutex#1 ready_mutex#49
	ready_mutex#1 ready_mutex#53
	ready_mutex#1 ready_mutex#55
	ready_mutex#1 ready_mutex#59
	ready_mutex#1 ready_mutex#61
	ready_mutex#1 ready_mutex#65
	ready_mutex#1 ready_mutex#67
	ready_mutex#1 ready_mutex#71
	ready_mutex#1 ready_mutex#73
	ready_mutex#1 ready_mutex#77
	ready_mutex#1 ready_mutex#79
	ready_mutex#1 ready_mutex#83
	ready_mutex#1 ready_mutex#85
	ready_mutex#1 ready_mutex#89
	ready_mutex#1 ready_mutex#91
	ready_mutex#1 ready_mutex#95
	ready_mutex#1 ready_mutex#97
	ready_mutex#1 ready_mutex#101
	ready_mutex#1 ready_mutex#103
	ready_mutex#1 ready_mutex#107
	ready_mutex#1 ready_mutex#109
	ready_mutex#1 ready_mutex#113
	ready_mutex#1 ready_mutex#115
	ready_mutex#1 ready_mutex#119
	ready_mutex#1 ready_mutex#121
	ready_mutex#1 ready_mutex#125
	ready_mutex#1 ready_mutex#127
	ready_mutex#1 ready_mutex#131
	ready_mutex#1 ready_mutex#133
	ready_mutex#1 ready_mutex#137
	ready_mutex#1 ready_mutex#139
	ready_mutex#1 ready_mutex#143
	ready_mutex#1 ready_mutex#145
	ready_mutex#1 ready_mutex#149
	ready_mutex#1 ready_mutex#151
	ready_mutex#1 ready_mutex#155
	ready_mutex#1 ready_mutex#157
	ready_mutex#1 ready_mutex#161
	ready_mutex#1 ready_mutex#163
	ready_mutex#1 ready_mutex#167
	ready_mutex#1 ready_mutex#169
	ready_mutex#1 ready_mutex#173
	ready_mutex#1 ready_mutex#175
	ready_mutex#1 ready_mutex#179
	ready_mutex#1 ready_mutex#181
	ready_mutex#1 ready_mutex#185
	ready_mutex#1 ready_mutex#187
Runtime Symex: 2.24726s
Adding SC constraints
Shared __CPROVER_threads_exited: 10R/6W
Shared __CPROVER_next_thread_id: 9R/6W
Shared __CPROVER_memory_leak: 1R/3W
Shared data: 5R/2W
Shared ready: 25R/2W
Shared ready_mutex: 62R/63W
Shared ready_cond: 26R/27W
Shared symex_dynamic::dynamic_object1: 9R/6W
size of program expression: 6659 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.206055s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.632655s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.0217298s
