./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c


--------------------------------------------------------------------------------


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/weaver/parallel-misc-5.wvr.c
Converting
Type-checking parallel-misc-5.wvr
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 parallel-misc-5.wvr file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c line 22
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 3 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
[Warning][Unknown] Invalidating expressions: AddrOf(Var(pos,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:105:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(c1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:106:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(c2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:107:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:108:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:108:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(v_assert, NoOffset)), AddrOf(Var(c2, NoOffset)), AddrOf(Var(c1, NoOffset)), AddrOf(Var(pos, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:108:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(v_assert, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:108:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:46:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:46:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(v_assert,
                                     NoOffset)), AddrOf(Var(c2, NoOffset)), AddrOf(Var(c1, NoOffset)), AddrOf(Var(pos, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:46:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:46:5)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:72:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:72:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(v_assert,
                                     NoOffset)), AddrOf(Var(c2, NoOffset)), AddrOf(Var(c1, NoOffset)), AddrOf(Var(pos, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:72:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:72:5)
[Warning][Race] Memory location v_assert@parallel-misc-5.wvr.c:39:7 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:114:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:43:3)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:114:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:60:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:115:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:69:3)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:115:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:86:5)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:116:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:95:3)
[Warning][Race] Memory location pos@parallel-misc-5.wvr.c:38:5 (race with conf. 110):
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:114:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:48:7)
  read with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:114:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:55:7)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:115:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:74:7)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:115:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:81:7)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:116:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:95:3)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:114:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:48:7)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:114:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:55:7)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:115:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:74:7)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:115:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c:81:7)

Summary for all memory locations:
	safe:            2
	vulnerable:      0
	unsafe:          2
	-------------------
	total:           4
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
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Unwinding loop thread1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c line 45 function thread1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Not unwinding loop thread1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c line 45 function thread1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Unwinding loop thread2.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c line 71 function thread2 thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Not unwinding loop thread2.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c line 71 function thread2 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/weaver/parallel-misc-5.wvr.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 105 106 43 44 46 47 48 49 55 56 60 61 69 70 72 73 74 75 81 82 86 87 95 96 
The number of races before goblint filter: 80
The number of races after goblint filter: 1
Race categories: 1
	105(1) - 96(1) pos:
		pos#2 pos#27
Runtime Symex: 0.361489s
Adding SC constraints
Shared __CPROVER_threads_exited: 6R/4W
Shared __CPROVER_next_thread_id: 5R/4W
Shared pos: 9R/10W
Shared c1: 4R/6W
Shared c2: 4R/6W
Shared v_assert: 6R/3W
Shared main::1::t1!0@1: 2R/2W
Shared main::1::t2!0@1: 2R/2W
Shared main::1::t3!0@1: 2R/2W
size of program expression: 688 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.00331752s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0051382s
Set Deagle solver's graph
WARNING: Find cycle during set_graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.00167454s
Solving with Deagle's Closure solver
8652 variables, 24221 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 0.00169287s
Runtime decision procedure: 0.0163862s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-misc-5.wvr.c function main
[nodatarace.assertion.0] line 116 No data races on variable pos between line 105 and line 96: SUCCESS

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