./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.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-deagle/airline-5.i
Converting
Type-checking airline-5
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 airline-5 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i line 407
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 1 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
[Warning][Race] Memory location numberOfSeatsSold@airline-5.i:717:5 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i:722:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i:752:3)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i:729:7)
[Warning][Race] Memory location stopSales@airline-5.i:718:5 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i:721:3)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i:725:7)

Summary for all memory locations:
	safe:            0
	vulnerable:      0
	unsafe:          2
	-------------------
	total:           2
argc''s upper bound is 1073741824
set limit type 4
Use SV-COMP unwinding strategy: 6
Deagle's solver is set!!!!!!
Unwinding loop main.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i line 746 function main thread 0
Unwinding loop main.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i line 746 function main thread 0
Unwinding loop main.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i line 746 function main thread 0
Unwinding loop main.0 iteration 4 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i line 746 function main thread 0
Unwinding loop main.0 iteration 5 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i line 746 function main thread 0
Unwinding loop main.1 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i line 749 function main thread 0
Unwinding loop main.1 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i line 749 function main thread 0
Unwinding loop main.1 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i line 749 function main thread 0
Unwinding loop main.1 iteration 4 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i line 749 function main thread 0
Unwinding loop main.1 iteration 5 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i line 749 function main thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
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-deagle/airline-5.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 721 722 723 725 726 729 730 752 753 
The number of races before goblint filter: 75
The number of races after goblint filter: 45
Race categories: 5
	722(1) - 730(1) numberOfSeatsSold:
		numberOfSeatsSold#4 numberOfSeatsSold#7
		numberOfSeatsSold#4 numberOfSeatsSold#9
		numberOfSeatsSold#4 numberOfSeatsSold#11
		numberOfSeatsSold#4 numberOfSeatsSold#13
		numberOfSeatsSold#6 numberOfSeatsSold#9
		numberOfSeatsSold#6 numberOfSeatsSold#11
		numberOfSeatsSold#6 numberOfSeatsSold#13
		numberOfSeatsSold#8 numberOfSeatsSold#11
		numberOfSeatsSold#8 numberOfSeatsSold#13
		numberOfSeatsSold#10 numberOfSeatsSold#13
	730(1) - 722(1) numberOfSeatsSold:
		numberOfSeatsSold#5 numberOfSeatsSold#6
		numberOfSeatsSold#5 numberOfSeatsSold#8
		numberOfSeatsSold#5 numberOfSeatsSold#10
		numberOfSeatsSold#5 numberOfSeatsSold#12
		numberOfSeatsSold#7 numberOfSeatsSold#8
		numberOfSeatsSold#7 numberOfSeatsSold#10
		numberOfSeatsSold#7 numberOfSeatsSold#12
		numberOfSeatsSold#9 numberOfSeatsSold#10
		numberOfSeatsSold#9 numberOfSeatsSold#12
		numberOfSeatsSold#11 numberOfSeatsSold#12
	752(1) - 730(1) numberOfSeatsSold:
		numberOfSeatsSold#3 numberOfSeatsSold#5
		numberOfSeatsSold#3 numberOfSeatsSold#7
		numberOfSeatsSold#3 numberOfSeatsSold#9
		numberOfSeatsSold#3 numberOfSeatsSold#11
		numberOfSeatsSold#3 numberOfSeatsSold#13
	721(1) - 726(1) stopSales:
		stopSales#3 stopSales#6
		stopSales#3 stopSales#8
		stopSales#3 stopSales#10
		stopSales#3 stopSales#12
		stopSales#5 stopSales#8
		stopSales#5 stopSales#10
		stopSales#5 stopSales#12
		stopSales#7 stopSales#10
		stopSales#7 stopSales#12
		stopSales#9 stopSales#12
	726(1) - 721(1) stopSales:
		stopSales#4 stopSales#5
		stopSales#4 stopSales#7
		stopSales#4 stopSales#9
		stopSales#4 stopSales#11
		stopSales#6 stopSales#7
		stopSales#6 stopSales#9
		stopSales#6 stopSales#11
		stopSales#8 stopSales#9
		stopSales#8 stopSales#11
		stopSales#10 stopSales#11
Runtime Symex: 0.458154s
Adding SC constraints
Shared __CPROVER_threads_exited: 10R/6W
Shared __CPROVER_next_thread_id: 9R/6W
Shared numberOfSeatsSold: 6R/7W
Shared stopSales: 5R/7W
Shared main::1::salethreads!0@1[[0]]: 10R/1W
Shared main::1::salethreads!0@1[[1]]: 10R/2W
Shared main::1::salethreads!0@1[[2]]: 10R/2W
Shared main::1::salethreads!0@1[[3]]: 10R/2W
Shared main::1::salethreads!0@1[[4]]: 10R/2W
size of program expression: 972 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.00551587s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00735818s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.00861599s
Solving with Deagle's Closure solver
15853 variables, 44851 clauses
ClosureSolver finishes with 10 conflicts, 3554 decisions, and 19177 propagations. 86 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0120563s
Runtime decision procedure: 0.0345157s
Running propositional reduction
Solving with Deagle's Closure solver
15853 variables, 33482 clauses
ClosureSolver finishes with 70 conflicts, 6981 decisions, and 33309 propagations. 86 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00127591s
Runtime decision procedure: 0.00130083s
Running propositional reduction
Solving with Deagle's Closure solver
15853 variables, 33483 clauses
ClosureSolver finishes with 71 conflicts, 9717 decisions, and 44772 propagations. 86 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00104113s
Runtime decision procedure: 0.00106398s
Running propositional reduction
Solving with Deagle's Closure solver
15853 variables, 33483 clauses
ClosureSolver finishes with 1348 conflicts, 11683 decisions, and 737723 propagations. 1012 theory propagations and 216 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.143268s
Runtime decision procedure: 0.14329s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-5.i function main
[nodatarace.assertion.0] line 746 No data races on variable numberOfSeatsSold between line 722 and line 730: FAILURE
[nodatarace.assertion.1] line 746 No data races on variable numberOfSeatsSold between line 730 and line 722: FAILURE
[nodatarace.assertion.2] line 746 No data races on variable numberOfSeatsSold between line 752 and line 730: SUCCESS
[nodatarace.assertion.3] line 746 No data races on variable stopSales between line 721 and line 726: FAILURE
[nodatarace.assertion.4] line 746 No data races on variable stopSales between line 726 and line 721: FAILURE

** 4 of 5 failed (4 iterations)
VERIFICATION FAILED
