./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.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/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i
Converting
Type-checking thread-join-counter-outer-race-2
Generating GOTO Program
Adding CPROVER library (x86_64)
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 thread-join-counter-outer-race-2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 605
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_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 thread-join-counter-outer-race-2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 505
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 thread-join-counter-outer-race-2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 392
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_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 thread-join-counter-outer-race-2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 510
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
set limit type 3
Use SV-COMP unwinding strategy: 6
Deagle's solver is set!!!!!!
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
**** WARNING: no body for function pthread_detach
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i:694:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(data,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i:689:3)
[Debug][Analyzer] Base EvalInt tid query answering bot instead of {([main], {thread@/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i:702:5})} (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i:702:5)
[Warning][Unknown] Function definition missing for pthread_detach (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i:702:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i:702:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(data_mutex,
                                     NoOffset)), AddrOf(Var(data, NoOffset)), AddrOf(Var(threads_alive_cond, NoOffset)), AddrOf(Var(threads_alive_mutex, NoOffset)), AddrOf(Var(threads_alive, NoOffset)), Lval(Var(tid, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i:702:5)
[Warning][Race] Memory location data@thread-join-counter-outer-race-2.i:681:5 (race with conf. 110):
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i:708:3)
  write with {lock:data_mutex} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i:689:3)

Summary for all memory locations:
	safe:           14
	vulnerable:      0
	unsafe:          1
	-------------------
	total:          15
Unwinding loop main.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 696 function main thread 0
Unwinding loop main.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 696 function main thread 0
Unwinding loop main.0 iteration 3 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 696 function main thread 0
Unwinding loop main.0 iteration 4 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 696 function main thread 0
Unwinding loop main.0 iteration 5 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 696 function main thread 0
Not unwinding loop main.0 iteration 6 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 696 function main thread 0
Unwinding loop main.1 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 705 function main thread 0
Unwinding loop main.1 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 705 function main thread 0
Unwinding loop main.1 iteration 3 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 705 function main thread 0
Unwinding loop main.1 iteration 4 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 705 function main thread 0
Unwinding loop main.1 iteration 5 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 705 function main thread 0
Not unwinding loop main.1 iteration 6 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i line 705 function main thread 0
aborting path on assume(false) at file <builtin-library-__spawned_thread> line 34 function __spawned_thread thread 6
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/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 689 690 694 695 702 703 708 709 
The number of races before goblint filter: 282
The number of races after goblint filter: 21
Race categories: 2
	689(1) - 689(1) data:
		data#3 data#4
		data#3 data#5
		data#3 data#6
		data#3 data#7
		data#3 data#8
		data#4 data#5
		data#4 data#6
		data#4 data#7
		data#4 data#8
		data#5 data#6
		data#5 data#7
		data#5 data#8
		data#6 data#7
		data#6 data#8
		data#7 data#8
	708(1) - 689(1) data:
		data#2 data#3
		data#2 data#4
		data#2 data#5
		data#2 data#6
		data#2 data#7
		data#2 data#8
Runtime Symex: 1.38133s
Adding SC constraints
Shared __CPROVER_threads_exited: 6R/7W
Shared __CPROVER_next_thread_id: 5R/7W
Shared data: 1R/7W
Shared threads_alive: 17R/13W
Shared threads_alive_mutex: 24R/27W
Shared threads_alive_cond: 12R/13W
Shared data_mutex: 12R/13W
Shared main::1::1::1::tid!0@1: 1R/3W
Shared main::1::1::1::tid!0@2: 1R/3W
Shared main::1::1::1::tid!0@3: 1R/3W
Shared main::1::1::1::tid!0@4: 1R/3W
Shared main::1::1::1::tid!0@5: 1R/3W
Shared main::1::1::1::tid!0@6: 1R/3W
size of program expression: 2266 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.057193s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.136612s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.00352052s
Solving with Deagle's Closure solver
191131 variables, 884919 clauses
ClosureSolver finishes with 864 conflicts, 290093 decisions, and 4283710 propagations. 15438 theory propagations and 304 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.777497s
Runtime decision procedure: 0.940347s
Running propositional reduction
Solving with Deagle's Closure solver
191131 variables, 880881 clauses
ClosureSolver finishes with 4588 conflicts, 297540 decisions, and 7558266 propagations. 24495 theory propagations and 1169 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.805512s
Runtime decision procedure: 0.805548s

** Results:
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-outer-race-2.i function main
[nodatarace.assertion.0] line 702 No data races on variable data between line 689 and line 689: SUCCESS
[nodatarace.assertion.1] line 702 No data races on variable data between line 708 and line 689: FAILURE

** 1 of 2 failed (2 iterations)
VERIFICATION FAILED
