./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.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/fib_unsafe-12-racy.i
Converting
Type-checking fib_unsafe-12-racy
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 fib_unsafe-12-racy file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 403
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
argc''s upper bound is 1073741824
set limit type 4
Use SV-COMP unwinding strategy: 27
Deagle's solver is set!!!!!!
Unwinding loop fib.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 4 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 5 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 6 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 7 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 8 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 9 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 10 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 11 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 12 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 13 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 14 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 15 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 16 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 17 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 18 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 19 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 20 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 21 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 22 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 23 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 24 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 25 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Unwinding loop fib.0 iteration 26 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
Not unwinding loop fib.0 iteration 27 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 706 function fib thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
Unwinding loop t1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 4 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 5 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 6 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 7 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 8 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 9 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 10 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 11 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 12 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 13 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 14 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 15 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 16 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 17 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 18 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 19 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 20 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 21 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 22 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 23 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 24 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 25 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t1.0 iteration 26 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Not unwinding loop t1.0 iteration 27 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 688 function t1 thread 1
Unwinding loop t2.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-bench[Warning][Race] Memory location j@fib_unsafe-12-racy.i:683:8 (race with conf. 110):
  read with {thread:([t1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:722:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:690:5)
  read with {thread:([t2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:723:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:698:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:725:3)
  write with {thread:([t2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:723:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:698:5)
[Warning][Race] Memory location i@fib_unsafe-12-racy.i:683:5 (race with conf. 110):
  read with {thread:([t1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:722:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:690:5)
  read with {thread:([t2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:723:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:698:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:725:3)
  write with {thread:([t1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:722:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i:690:5)

Summary for all memory locations:
	safe:            6
	vulnerable:      0
	unsafe:          2
	-------------------
	total:           8
marks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 4 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 5 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 6 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 7 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 8 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 9 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 10 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 11 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 12 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 13 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 14 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 15 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 16 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 17 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 18 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 19 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 20 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 21 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 22 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 23 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 24 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 25 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Unwinding loop t2.0 iteration 26 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 thread 2
Not unwinding loop t2.0 iteration 27 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i line 696 function t2 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/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 690 691 698 699 725 726 
The number of races before goblint filter: 380
The number of races after goblint filter: 54
Race categories: 2
	725(1) - 691(1) i:
		i#3 i#6
		i#3 i#9
		i#3 i#12
		i#3 i#15
		i#3 i#18
		i#3 i#21
		i#3 i#24
		i#3 i#27
		i#3 i#30
		i#3 i#33
		i#3 i#36
		i#3 i#39
		i#3 i#42
		i#3 i#45
		i#3 i#48
		i#3 i#51
		i#3 i#54
		i#3 i#57
		i#3 i#60
		i#3 i#63
		i#3 i#66
		i#3 i#69
		i#3 i#72
		i#3 i#75
		i#3 i#78
		i#3 i#81
		i#3 i#84
	725(1) - 699(1) j:
		j#3 j#60
		j#3 j#63
		j#3 j#66
		j#3 j#69
		j#3 j#72
		j#3 j#75
		j#3 j#78
		j#3 j#81
		j#3 j#84
		j#3 j#87
		j#3 j#90
		j#3 j#93
		j#3 j#96
		j#3 j#99
		j#3 j#102
		j#3 j#105
		j#3 j#108
		j#3 j#111
		j#3 j#114
		j#3 j#117
		j#3 j#120
		j#3 j#123
		j#3 j#126
		j#3 j#129
		j#3 j#132
		j#3 j#135
		j#3 j#138
Runtime Symex: 14.5494s
Adding SC constraints
Shared __CPROVER_threads_exited: 2R/3W
Shared __CPROVER_next_thread_id: 1R/3W
Shared i: 55R/29W
Shared j: 55R/29W
Shared p: 54R/29W
Shared q: 54R/29W
Shared cur: 54R/28W
Shared prev: 28R/28W
Shared next: 27R/28W
Shared x: 54R/29W
size of program expression: 8345 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.118348s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.200725s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.00388506s
Solving with Deagle's Closure solver
231708 variables, 1171508 clauses
ClosureSolver finishes with 1395 conflicts, 58339 decisions, and 4018163 propagations. 12005 theory propagations and 13 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.973541s
Runtime decision procedure: 1.29822s
Running propositional reduction
Solving with Deagle's Closure solver
231708 variables, 549219 clauses
ClosureSolver finishes with 1395 conflicts, 62639 decisions, and 4145866 propagations. 12160 theory propagations and 13 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0349064s
Runtime decision procedure: 0.0349409s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-12-racy.i function main
[nodatarace.assertion.0] line 723 No data races on variable i between line 725 and line 691: FAILURE
[nodatarace.assertion.1] line 723 No data races on variable j between line 725 and line 699: FAILURE

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