./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.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-barrier-loop.wvr.c
Converting
Type-checking parallel-barrier-loop.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-barrier-loop.wvr file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.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 6 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:215:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:215:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15,
                                     NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:215:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:215:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:216:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:216:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:216:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(y_1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:216:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:217:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:217:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:217:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(x_8, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:217:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:218:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:218:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:218:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(y_9, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:218:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:219:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:219:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:219:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_4, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:219:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:220:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:220:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:220:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_5, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:220:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:221:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:221:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:221:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_6, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:221:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:222:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:222:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:222:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_7, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:222:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:223:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:223:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:223:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_12, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:223:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:224:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:224:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:224:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_13, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:224:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:225:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:225:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:225:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_14, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:225:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_uint (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:226:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:226:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:226:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:226:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:227:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:227:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:227:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f1_2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:227:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:228:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:228:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:228:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f2_3, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:228:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:229:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:229:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:229:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f1_10, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:229:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:230:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:230:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15, NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:230:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(f2_11, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:230:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:44:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:44:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15,
                                     NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:44:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:44:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:78:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:78:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15,
                                     NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:78:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:78:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:128:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:128:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15,
                                     NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:128:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:128:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:162:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:162:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(temp_15,
                                     NoOffset)), AddrOf(Var(temp_14, NoOffset)), AddrOf(Var(temp_13, NoOffset)), AddrOf(Var(temp_12, NoOffset)), AddrOf(Var(temp_7, NoOffset)), AddrOf(Var(temp_6, NoOffset)), AddrOf(Var(temp_5, NoOffset)), AddrOf(Var(temp_4, NoOffset)), AddrOf(Var(f2_11, NoOffset)), AddrOf(Var(f1_10, NoOffset)), AddrOf(Var(f2_3, NoOffset)), AddrOf(Var(f1_2, NoOffset)), AddrOf(Var(y_9, NoOffset)), AddrOf(Var(x_8, NoOffset)), AddrOf(Var(y_1, NoOffset)), AddrOf(Var(x_0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:162:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:162:3)
[Warning][Race] Memory location f2_11@parallel-barrier-loop.wvr.c:39:26 (race with conf. 110):
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:204:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:140:5)
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:204:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:154:5)
  write with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:205:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:171:5)
  write with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:205:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:185:5)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:200:3)
[Warning][Race] Memory location f1_10@parallel-barrier-loop.wvr.c:39:19 (race with conf. 110):
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:205:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:174:5)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:205:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:188:5)
  write with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:204:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:137:5)
  write with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:204:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:151:5)
  write with {thread:([thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:199:3)
[Warning][Race] Memory location f2_3@parallel-barrier-loop.wvr.c:39:13 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:120:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:56:5)
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:120:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:70:5)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:121:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:87:5)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:121:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:101:5)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:116:3)
[Warning][Race] Memory location f1_2@parallel-barrier-loop.wvr.c:39:7 (race with conf. 110):
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:121:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:90:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:121:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:104:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:120:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:53:5)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:120:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:67:5)
  write with {thread:([thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:115:3)
[Warning][Race] Memory location x_8@parallel-barrier-loop.wvr.c:38:24 (race with conf. 110):
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:204:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:130:5)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:205:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:178:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:240:3)
  write with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:204:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:133:5)
  write with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:205:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:181:5)
[Warning][Race] Memory location x_0@parallel-barrier-loop.wvr.c:38:14 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:120:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:46:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:121:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:94:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:240:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:120:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:49:5)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:121:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:97:5)
[Warning][Race] Memory location y_9@parallel-barrier-loop.wvr.c:38:29 (race with conf. 110):
  read with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:204:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:144:5)
  read with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:205:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:164:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:240:3)
  write with {thread:([thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:204:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:147:5)
  write with {thread:([thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:205:3, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:237:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:167:5)
[Warning][Race] Memory location y_1@parallel-barrier-loop.wvr.c:38:19 (race with conf. 110):
  read with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:120:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:60:5)
  read with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:121:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:80:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:240:3)
  write with {thread:([thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:120:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:63:5)
  write with {thread:([thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:121:3, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:236:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c:83:5)

Summary for all memory locations:
	safe:            8
	vulnerable:      0
	unsafe:          8
	-------------------
	total:          16
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 0
Unwinding recursion pthread_create iteration 1
Unwinding recursion pthread_create iteration 1
Unwinding recursion pthread_create iteration 1
Unwinding recursion pthread_create iteration 1
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Unwinding loop thread2.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c line 44 function thread2 thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Not unwinding loop thread2.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c line 44 function thread2 thread 3
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
Unwinding loop thread3.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c line 78 function thread3 thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
Not unwinding loop thread3.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c line 78 function thread3 thread 4
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
Unwinding loop thread5.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c line 128 function thread5 thread 5
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 5
Not unwinding loop thread5.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c line 128 function thread5 thread 5
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
Unwinding loop thread6.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c line 162 function thread6 thread 6
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 6
Not unwinding loop thread6.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c line 162 function thread6 thread 6
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-barrier-loop.wvr.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 101 102 104 105 115 116 117 128 129 130 131 133 134 137 138 140 141 144 145 147 148 151 152 154 155 162 163 164 165 167 168 171 172 174 175 178 179 181 182 185 186 188 189 199 200 201 215 216 240 241 44 45 46 47 49 50 53 54 56 57 60 61 63 64 67 68 70 71 78 79 80 81 83 84 87 88 90 91 94 95 97 98 
The number of races before goblint filter: 232
The number of races after goblint filter: 48
Race categories: 16
	215(1) - 47(1) x_0:
		x_0#2 x_0#5
		x_0#2 x_0#8
	215(1) - 50(1) x_0:
		x_0#2 x_0#7
		x_0#2 x_0#10
	215(1) - 95(1) x_0:
		x_0#2 x_0#11
		x_0#2 x_0#14
	215(1) - 98(1) x_0:
		x_0#2 x_0#13
		x_0#2 x_0#16
	240(1) - 50(1) x_0:
		x_0#3 x_0#7
		x_0#3 x_0#10
		x_0#4 x_0#7
		x_0#4 x_0#10
	240(1) - 98(1) x_0:
		x_0#3 x_0#13
		x_0#3 x_0#16
		x_0#4 x_0#13
		x_0#4 x_0#16
	240(1) - 134(1) x_8:
		x_8#3 x_8#7
		x_8#3 x_8#10
		x_8#4 x_8#7
		x_8#4 x_8#10
	240(1) - 182(1) x_8:
		x_8#3 x_8#13
		x_8#3 x_8#16
		x_8#4 x_8#13
		x_8#4 x_8#16
	216(1) - 61(1) y_1:
		y_1#2 y_1#5
		y_1#2 y_1#8
	216(1) - 64(1) y_1:
		y_1#2 y_1#7
		y_1#2 y_1#10
	216(1) - 81(1) y_1:
		y_1#2 y_1#11
		y_1#2 y_1#14
	216(1) - 84(1) y_1:
		y_1#2 y_1#13
		y_1#2 y_1#16
	240(1) - 64(1) y_1:
		y_1#3 y_1#7
		y_1#3 y_1#10
		y_1#4 y_1#7
		y_1#4 y_1#10
	240(1) - 84(1) y_1:
		y_1#3 y_1#13
		y_1#3 y_1#16
		y_1#4 y_1#13
		y_1#4 y_1#16
	240(1) - 148(1) y_9:
		y_9#3 y_9#7
		y_9#3 y_9#10
		y_9#4 y_9#7
		y_9#4 y_9#10
	240(1) - 168(1) y_9:
		y_9#3 y_9#13
		y_9#3 y_9#16
		y_9#4 y_9#13
		y_9#4 y_9#16
Runtime Symex: 2.17306s
Adding SC constraints
Shared __CPROVER_threads_exited: 12R/7W
Shared __CPROVER_next_thread_id: 11R/7W
Shared x_0: 6R/6W
Shared y_1: 6R/6W
Shared x_8: 6R/6W
Shared y_9: 6R/6W
Shared f1_2: 4R/7W
Shared f2_3: 4R/7W
Shared f1_10: 4R/7W
Shared f2_11: 4R/7W
Shared temp_4: 2R/4W
Shared temp_5: 2R/4W
Shared temp_6: 2R/4W
Shared temp_7: 2R/4W
Shared temp_12: 2R/4W
Shared temp_13: 2R/4W
Shared temp_14: 2R/4W
Shared temp_15: 2R/4W
Shared main::1::t1!0@1: 2R/2W
Shared main::1::t4!0@1: 2R/2W
Shared thread1::1::t2!1@1: 2R/3W
Shared thread1::1::t3!1@1: 2R/3W
Shared thread4::1::t5!2@1: 2R/3W
Shared thread4::1::t6!2@1: 2R/3W
size of program expression: 1732 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.00924103s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0112606s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.0134008s
Solving with Deagle's Closure solver
23520 variables, 80967 clauses
ClosureSolver finishes with 8216 conflicts, 17693 decisions, and 6755434 propagations. 12430 theory propagations and 391 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 1.49005s
Runtime decision procedure: 1.52641s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier-loop.wvr.c function thread4
[nodatarace.assertion.0] line 205 No data races on variable x_0 between line 215 and line 47: SUCCESS
[nodatarace.assertion.1] line 205 No data races on variable x_0 between line 215 and line 50: SUCCESS
[nodatarace.assertion.2] line 205 No data races on variable x_0 between line 215 and line 95: SUCCESS
[nodatarace.assertion.3] line 205 No data races on variable x_0 between line 215 and line 98: SUCCESS
[nodatarace.assertion.4] line 205 No data races on variable x_0 between line 240 and line 50: SUCCESS
[nodatarace.assertion.5] line 205 No data races on variable x_0 between line 240 and line 98: SUCCESS
[nodatarace.assertion.6] line 205 No data races on variable x_8 between line 240 and line 134: SUCCESS
[nodatarace.assertion.7] line 205 No data races on variable x_8 between line 240 and line 182: SUCCESS
[nodatarace.assertion.8] line 205 No data races on variable y_1 between line 216 and line 61: SUCCESS
[nodatarace.assertion.9] line 205 No data races on variable y_1 between line 216 and line 64: SUCCESS
[nodatarace.assertion.10] line 205 No data races on variable y_1 between line 216 and line 81: SUCCESS
[nodatarace.assertion.11] line 205 No data races on variable y_1 between line 216 and line 84: SUCCESS
[nodatarace.assertion.12] line 205 No data races on variable y_1 between line 240 and line 64: SUCCESS
[nodatarace.assertion.13] line 205 No data races on variable y_1 between line 240 and line 84: SUCCESS
[nodatarace.assertion.14] line 205 No data races on variable y_9 between line 240 and line 148: SUCCESS
[nodatarace.assertion.15] line 205 No data races on variable y_9 between line 240 and line 168: SUCCESS

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