./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.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-inner-race.i
Converting
Type-checking thread-join-counter-inner-race
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 thread-join-counter-inner-race file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.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-inner-race file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.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-inner-race file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.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
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
**** 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-inner-race.i:698:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(data,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:689:5)
[Debug][Analyzer] Base EvalInt tid query answering bot instead of {([main], {thread@/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:703:5})} (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:703:5)
[Warning][Unknown] Function definition missing for pthread_detach (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:703:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:703:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(data_mutex,
                                     NoOffset)), AddrOf(Var(data, NoOffset)), AddrOf(Var(keep_alive_mutex, NoOffset)), AddrOf(Var(keep_alive, NoOffset)), AddrOf(Var(threads_alive, NoOffset)), Lval(Var(tid, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:703:5)
[Warning][Race] Memory location data@thread-join-counter-inner-race.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-inner-race.i:710:3)
  write with {lock:data_mutex} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:689:5)
[Warning][Race] Memory location threads_alive@thread-join-counter-inner-race.i:678:5 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:684:3)
  read with {} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:694:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:705:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:709:3)
  write with {} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:684:3)
  write with {} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i:694:3)

Summary for all memory locations:
	safe:            1
	vulnerable:      0
	unsafe:          2
	-------------------
	total:           3
Unwinding loop main.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i line 700 function main thread 0
Not unwinding loop main.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i line 700 function main thread 0
replacing self-loop at file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i line 705 function main by assume(!TRUE)
replacing self-loop at file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i line 709 function main by assume(!TRUE)
Unwinding loop thread.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i line 686 function thread thread 1
Not unwinding loop thread.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i line 686 function thread thread 1
aborting path on assume(false) at file <builtin-library-__spawned_thread> line 34 function __spawned_thread thread 2
Unwinding loop thread.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i line 686 function thread thread 2
Not unwinding loop thread.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i line 686 function thread 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/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 684 685 689 690 694 695 703 704 705 706 709 710 711 
The number of races before goblint filter: 88
The number of races after goblint filter: 28
Race categories: 10
	689(1) - 689(1) data:
		data#3 data#5
		data#3 data#6
		data#4 data#5
		data#4 data#6
	710(1) - 689(1) data:
		data#2 data#3
		data#2 data#4
		data#2 data#5
		data#2 data#6
	684(1) - 684(1) threads_alive:
		threads_alive#4 threads_alive#9
		threads_alive#5 threads_alive#8
		threads_alive#5 threads_alive#9
	684(1) - 694(1) threads_alive:
		threads_alive#4 threads_alive#11
		threads_alive#5 threads_alive#10
		threads_alive#5 threads_alive#11
	694(1) - 684(1) threads_alive:
		threads_alive#6 threads_alive#9
		threads_alive#7 threads_alive#8
		threads_alive#7 threads_alive#9
	694(1) - 694(1) threads_alive:
		threads_alive#6 threads_alive#11
		threads_alive#7 threads_alive#10
		threads_alive#7 threads_alive#11
	705(1) - 684(1) threads_alive:
		threads_alive#2 threads_alive#5
		threads_alive#2 threads_alive#9
	705(1) - 694(1) threads_alive:
		threads_alive#2 threads_alive#7
		threads_alive#2 threads_alive#11
	709(1) - 684(1) threads_alive:
		threads_alive#3 threads_alive#5
		threads_alive#3 threads_alive#9
	709(1) - 694(1) threads_alive:
		threads_alive#3 threads_alive#7
		threads_alive#3 threads_alive#11
Runtime Symex: 0.471551s
Adding SC constraints
Shared __CPROVER_threads_exited: 2R/3W
Shared __CPROVER_next_thread_id: 1R/3W
Shared data: 1R/5W
Shared threads_alive: 6R/5W
Shared keep_alive: 4R/2W
Shared keep_alive_mutex: 14R/15W
Shared data_mutex: 8R/9W
Shared main::1::1::1::tid!0@1: 1R/3W
Shared main::1::1::1::tid!0@2: 1R/3W
size of program expression: 811 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0100062s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0308834s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.000236183s
Solving with Deagle's Closure solver
46992 variables, 201790 clauses
ClosureSolver finishes with 50 conflicts, 45446 decisions, and 248727 propagations. 7 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0419251s
Runtime decision procedure: 0.0835606s
Running propositional reduction
Solving with Deagle's Closure solver
46992 variables, 200584 clauses
ClosureSolver finishes with 119 conflicts, 50511 decisions, and 390794 propagations. 352 theory propagations and 24 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0248766s
Runtime decision procedure: 0.0249257s
Running propositional reduction
Solving with Deagle's Closure solver
46992 variables, 200585 clauses
ClosureSolver finishes with 125 conflicts, 54150 decisions, and 450673 propagations. 376 theory propagations and 25 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00886642s
Runtime decision procedure: 0.00890912s
Running propositional reduction
Solving with Deagle's Closure solver
46992 variables, 200586 clauses
ClosureSolver finishes with 127 conflicts, 56805 decisions, and 498277 propagations. 400 theory propagations and 25 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0082862s
Runtime decision procedure: 0.00832583s
Running propositional reduction
Solving with Deagle's Closure solver
46992 variables, 200587 clauses
ClosureSolver finishes with 131 conflicts, 60651 decisions, and 551484 propagations. 404 theory propagations and 27 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00758007s
Runtime decision procedure: 0.00761881s
Running propositional reduction
Solving with Deagle's Closure solver
46992 variables, 200588 clauses
ClosureSolver finishes with 143 conflicts, 60667 decisions, and 556799 propagations. 404 theory propagations and 27 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.000640941s
Runtime decision procedure: 0.000658212s

** Results:
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/thread-join-counter-inner-race.i function main
[nodatarace.assertion.0] line 703 No data races on variable data between line 689 and line 689: SUCCESS
[nodatarace.assertion.1] line 703 No data races on variable data between line 710 and line 689: FAILURE
[nodatarace.assertion.2] line 703 No data races on variable threads_alive between line 684 and line 684: FAILURE
[nodatarace.assertion.3] line 703 No data races on variable threads_alive between line 684 and line 694: SUCCESS
[nodatarace.assertion.4] line 703 No data races on variable threads_alive between line 694 and line 684: SUCCESS
[nodatarace.assertion.5] line 703 No data races on variable threads_alive between line 694 and line 694: SUCCESS
[nodatarace.assertion.6] line 703 No data races on variable threads_alive between line 705 and line 684: FAILURE
[nodatarace.assertion.7] line 703 No data races on variable threads_alive between line 705 and line 694: SUCCESS
[nodatarace.assertion.8] line 703 No data races on variable threads_alive between line 709 and line 684: FAILURE
[nodatarace.assertion.9] line 703 No data races on variable threads_alive between line 709 and line 694: FAILURE

** 5 of 10 failed (6 iterations)
VERIFICATION FAILED
