./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-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/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i
Converting
Type-checking fkp2013_variant-2
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 fkp2013_variant-2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-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 *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
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i:713:5)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i:55:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i:60:1)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i:65:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i:70:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i:75:1)
[Warning][Race] Memory location x@fkp2013_variant-2.i:697:14 (race with conf. 110):
  read with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i:716:5, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i:700:5)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i:705:5)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i:706:5)

Summary for all memory locations:
	safe:            1
	vulnerable:      0
	unsafe:          1
	-------------------
	total:           2
argc''s upper bound is 1073741824
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
Unwinding loop main.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i line 716 function main thread 0
Not unwinding loop main.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i line 716 function main thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-__spawned_thread> line 34 function __spawned_thread thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
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-lit/fkp2013_variant-2.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 700 701 705 706 707 713 714 
The number of races before goblint filter: 33
The number of races after goblint filter: 13
Race categories: 6
	713(1) - 700(1) n:
		n#2 n#5
		n#2 n#6
		n#2 n#7
		n#2 n#8
	700(1) - 706(1) x:
		x#3 x#6
		x#4 x#6
		x#3 x#8
		x#4 x#8
	705(1) - 706(1) x:
		x#5 x#8
	706(1) - 700(1) x:
		x#6 x#9
		x#6 x#10
	706(1) - 705(1) x:
		x#6 x#7
	706(1) - 706(1) x:
		x#6 x#8
Runtime Symex: 0.157177s
Adding SC constraints
Shared __CPROVER_threads_exited: 3R/4W
Shared __CPROVER_next_thread_id: 2R/4W
Shared x: 6R/4W
Shared n: 6R/2W
size of program expression: 370 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.000957308s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00197726s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.000594271s
Solving with Deagle's Closure solver
3483 variables, 7842 clauses
ClosureSolver finishes with 5 conflicts, 1098 decisions, and 3805 propagations. 19 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00104137s
Runtime decision procedure: 0.0080969s
Running propositional reduction
Solving with Deagle's Closure solver
3483 variables, 6918 clauses
ClosureSolver finishes with 5 conflicts, 2143 decisions, and 6410 propagations. 19 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000212344s
Runtime decision procedure: 0.000223115s
Running propositional reduction
Solving with Deagle's Closure solver
3483 variables, 6919 clauses
ClosureSolver finishes with 6 conflicts, 3212 decisions, and 9155 propagations. 19 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000253764s
Runtime decision procedure: 0.000263874s
Running propositional reduction
Solving with Deagle's Closure solver
3483 variables, 6920 clauses
ClosureSolver finishes with 6 conflicts, 4274 decisions, and 11508 propagations. 19 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000201984s
Runtime decision procedure: 0.000211604s
Running propositional reduction
Solving with Deagle's Closure solver
3483 variables, 6920 clauses
ClosureSolver finishes with 6 conflicts, 5342 decisions, and 13861 propagations. 19 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000198284s
Runtime decision procedure: 0.000208195s
Running propositional reduction
Solving with Deagle's Closure solver
3483 variables, 6920 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 3.651e-06s
Runtime decision procedure: 9.87e-06s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fkp2013_variant-2.i function main
[nodatarace.assertion.0] line 716 No data races on variable n between line 713 and line 700: SUCCESS
[nodatarace.assertion.1] line 716 No data races on variable x between line 700 and line 706: FAILURE
[nodatarace.assertion.2] line 716 No data races on variable x between line 705 and line 706: FAILURE
[nodatarace.assertion.3] line 716 No data races on variable x between line 706 and line 700: FAILURE
[nodatarace.assertion.4] line 716 No data races on variable x between line 706 and line 705: FAILURE
[nodatarace.assertion.5] line 716 No data races on variable x between line 706 and line 706: FAILURE

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