./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.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-C-DAC/pthread-demo-datarace-3.i
Converting
Type-checking pthread-demo-datarace-3
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 pthread-demo-datarace-3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 390
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
set limit type 4
Use SV-COMP unwinding strategy: 21
Deagle's solver is set!!!!!!
pointer handling for concurrency is unsound
Unwinding loop main.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 4 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 5 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 6 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 7 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 8 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 9 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 10 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 11 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 12 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 13 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 14 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 15 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 16 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 17 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 18 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 19 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
Unwinding loop main.0 iteration 20 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1352 function main thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
Unwinding loop thread_function_datarace.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i:68:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i:73:1)
[Warning][Race] Memory location myglobal@pthread-demo-datarace-3.i:1320:5 (race with conf. 110):
  read with {thread:([thread_function_datarace@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i:1342:5, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i:1328:9)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i:1355:9)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i:1362:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i:1363:5)
  write with {thread:([thread_function_datarace@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i:1342:5, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i:1333:9)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i:1355:9)

Summary for all memory locations:
	safe:            0
	vulnerable:      0
	unsafe:          1
	-------------------
	total:           1
-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 4 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 5 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 6 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 7 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 8 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 9 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 10 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 11 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 12 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 13 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 14 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 15 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 16 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 17 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 18 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 19 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
Unwinding loop thread_function_datarace.0 iteration 20 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i line 1325 function thread_function_datarace thread 1
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-C-DAC/pthread-demo-datarace-3.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 1328 1329 1333 1334 1355 1356 1362 1363 1364 
The number of races before goblint filter: 140
The number of races after goblint filter: 100
Race categories: 2
	1362(1) - 1334(1) myglobal:
		myglobal#62 myglobal#69
		myglobal#62 myglobal#72
		myglobal#62 myglobal#75
		myglobal#62 myglobal#78
		myglobal#62 myglobal#81
		myglobal#62 myglobal#84
		myglobal#62 myglobal#87
		myglobal#62 myglobal#90
		myglobal#62 myglobal#93
		myglobal#62 myglobal#96
		myglobal#62 myglobal#99
		myglobal#62 myglobal#102
		myglobal#62 myglobal#105
		myglobal#62 myglobal#108
		myglobal#62 myglobal#111
		myglobal#62 myglobal#114
		myglobal#62 myglobal#117
		myglobal#62 myglobal#120
		myglobal#62 myglobal#123
		myglobal#62 myglobal#126
		myglobal#63 myglobal#69
		myglobal#63 myglobal#72
		myglobal#63 myglobal#75
		myglobal#63 myglobal#78
		myglobal#63 myglobal#81
		myglobal#63 myglobal#84
		myglobal#63 myglobal#87
		myglobal#63 myglobal#90
		myglobal#63 myglobal#93
		myglobal#63 myglobal#96
		myglobal#63 myglobal#99
		myglobal#63 myglobal#102
		myglobal#63 myglobal#105
		myglobal#63 myglobal#108
		myglobal#63 myglobal#111
		myglobal#63 myglobal#114
		myglobal#63 myglobal#117
		myglobal#63 myglobal#120
		myglobal#63 myglobal#123
		myglobal#63 myglobal#126
	1363(1) - 1334(1) myglobal:
		myglobal#64 myglobal#69
		myglobal#64 myglobal#72
		myglobal#64 myglobal#75
		myglobal#64 myglobal#78
		myglobal#64 myglobal#81
		myglobal#64 myglobal#84
		myglobal#64 myglobal#87
		myglobal#64 myglobal#90
		myglobal#64 myglobal#93
		myglobal#64 myglobal#96
		myglobal#64 myglobal#99
		myglobal#64 myglobal#102
		myglobal#64 myglobal#105
		myglobal#64 myglobal#108
		myglobal#64 myglobal#111
		myglobal#64 myglobal#114
		myglobal#64 myglobal#117
		myglobal#64 myglobal#120
		myglobal#64 myglobal#123
		myglobal#64 myglobal#126
		myglobal#65 myglobal#69
		myglobal#65 myglobal#72
		myglobal#65 myglobal#75
		myglobal#65 myglobal#78
		myglobal#65 myglobal#81
		myglobal#65 myglobal#84
		myglobal#65 myglobal#87
		myglobal#65 myglobal#90
		myglobal#65 myglobal#93
		myglobal#65 myglobal#96
		myglobal#65 myglobal#99
		myglobal#65 myglobal#102
		myglobal#65 myglobal#105
		myglobal#65 myglobal#108
		myglobal#65 myglobal#111
		myglobal#65 myglobal#114
		myglobal#65 myglobal#117
		myglobal#65 myglobal#120
		myglobal#65 myglobal#123
		myglobal#65 myglobal#126
		myglobal#66 myglobal#69
		myglobal#66 myglobal#72
		myglobal#66 myglobal#75
		myglobal#66 myglobal#78
		myglobal#66 myglobal#81
		myglobal#66 myglobal#84
		myglobal#66 myglobal#87
		myglobal#66 myglobal#90
		myglobal#66 myglobal#93
		myglobal#66 myglobal#96
		myglobal#66 myglobal#99
		myglobal#66 myglobal#102
		myglobal#66 myglobal#105
		myglobal#66 myglobal#108
		myglobal#66 myglobal#111
		myglobal#66 myglobal#114
		myglobal#66 myglobal#117
		myglobal#66 myglobal#120
		myglobal#66 myglobal#123
		myglobal#66 myglobal#126
Runtime Symex: 0.824881s
Adding SC constraints
Shared __CPROVER_threads_exited: 2R/2W
Shared __CPROVER_next_thread_id: 1R/2W
Shared myglobal: 45R/41W
Shared main::1::mythread!0@1: 2R/2W
Shared printf::format!0@1: 1R/2W
Shared printf::format!0@2: 1R/2W
Shared printf::format!0@3: 1R/2W
Shared printf::format!0@4: 1R/2W
Shared printf::format!0@5: 1R/2W
Shared printf::format!0@6: 1R/2W
Shared printf::format!0@7: 1R/2W
Shared printf::format!0@8: 1R/2W
Shared printf::format!1@1: 1R/2W
Shared printf::format!1@2: 1R/2W
Shared printf::format!1@3: 1R/2W
Shared printf::format!1@4: 1R/2W
Shared printf::format!1@5: 1R/2W
Shared printf::format!1@6: 1R/2W
Shared printf::format!1@7: 1R/2W
Shared printf::format!1@8: 1R/2W
Shared printf::format!1@9: 1R/2W
Shared printf::format!1@10: 1R/2W
Shared printf::format!1@11: 1R/2W
Shared printf::format!1@12: 1R/2W
Shared printf::format!1@13: 1R/2W
Shared printf::format!1@14: 1R/2W
Shared printf::format!1@15: 1R/2W
Shared printf::format!1@16: 1R/2W
Shared printf::format!1@17: 1R/2W
Shared printf::format!1@18: 1R/2W
Shared printf::format!1@19: 1R/2W
Shared printf::format!1@20: 1R/2W
size of program expression: 2688 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0157879s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0400877s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.000405666s
Solving with Deagle's Closure solver
59703 variables, 243555 clauses
ClosureSolver finishes with 2 conflicts, 6 decisions, and 3686 propagations. 704 theory propagations and 0 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.00310154s
Runtime decision procedure: 0.0679987s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-demo-datarace-3.i function main
[nodatarace.assertion.0] line 1342 No data races on variable myglobal between line 1362 and line 1334: SUCCESS
[nodatarace.assertion.1] line 1342 No data races on variable myglobal between line 1363 and line 1334: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL
