./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.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-wmm/rfi006_power.oepc.i
Converting
Type-checking rfi006_power.oepc
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 rfi006_power.oepc file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i line 423
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] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:761:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:761:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice2, NoOffset)), AddrOf(Var(weak$$choice1, NoOffset)), AddrOf(Var(weak$$choice0, NoOffset)), AddrOf(Var(y, NoOffset)), AddrOf(Var(x$w_buff1_used, NoOffset)), AddrOf(Var(x$w_buff1, NoOffset)), AddrOf(Var(x$w_buff0_used, NoOffset)), AddrOf(Var(x$w_buff0, NoOffset)), AddrOf(Var(x$read_delayed_var, NoOffset)), AddrOf(Var(x$read_delayed, NoOffset)), AddrOf(Var(x$r_buff1_thd3, NoOffset)), AddrOf(Var(x$r_buff1_thd2, NoOffset)), AddrOf(Var(x$r_buff1_thd1, NoOffset)), AddrOf(Var(x$r_buff1_thd0, NoOffset)), AddrOf(Var(x$r_buff0_thd3, NoOffset)), AddrOf(Var(x$r_buff0_thd2, NoOffset)), AddrOf(Var(x$r_buff0_thd1, NoOffset)), AddrOf(Var(x$r_buff0_thd0, NoOffset)), AddrOf(Var(x$mem_tmp, NoOffset)), AddrOf(Var(x$flush_delayed, NoOffset)), AddrOf(Var(x, NoOffset)), AddrOf(Var(main$tmp_guard1, NoOffset)), AddrOf(Var(main$tmp_guard0, NoOffset)), AddrOf(Var(__unbuffered_p1_EBX, NoOffset)), AddrOf(Var(__unbuffered_p1_EAX, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed_var, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$mem_tmp, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$flush_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX, NoOffset)), AddrOf(Var(__unbuffered_cnt, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:761:3)
[Warning][Unknown] Unknown address in {&x$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:761:3)
[Warning][Unknown] Unknown address in {&__unbuffered_p0_EAX$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:761:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:761:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:762:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:762:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice2, NoOffset)), AddrOf(Var(weak$$choice1, NoOffset)), AddrOf(Var(weak$$choice0, NoOffset)), AddrOf(Var(y, NoOffset)), AddrOf(Var(x$w_buff1_used, NoOffset)), AddrOf(Var(x$w_buff1, NoOffset)), AddrOf(Var(x$w_buff0_used, NoOffset)), AddrOf(Var(x$w_buff0, NoOffset)), AddrOf(Var(x$read_delayed_var, NoOffset)), AddrOf(Var(x$read_delayed, NoOffset)), AddrOf(Var(x$r_buff1_thd3, NoOffset)), AddrOf(Var(x$r_buff1_thd2, NoOffset)), AddrOf(Var(x$r_buff1_thd1, NoOffset)), AddrOf(Var(x$r_buff1_thd0, NoOffset)), AddrOf(Var(x$r_buff0_thd3, NoOffset)), AddrOf(Var(x$r_buff0_thd2, NoOffset)), AddrOf(Var(x$r_buff0_thd1, NoOffset)), AddrOf(Var(x$r_buff0_thd0, NoOffset)), AddrOf(Var(x$mem_tmp, NoOffset)), AddrOf(Var(x$flush_delayed, NoOffset)), AddrOf(Var(x, NoOffset)), AddrOf(Var(main$tmp_guard1, NoOffset)), AddrOf(Var(main$tmp_guard0, NoOffset)), AddrOf(Var(__unbuffered_p1_EBX, NoOffset)), AddrOf(Var(__unbuffered_p1_EAX, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed_var, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$mem_tmp, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$flush_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX, NoOffset)), AddrOf(Var(__unbuffered_cnt, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:762:3)
[Warning][Unknown] Unknown address in {&x$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:762:3)
[Warning][Unknown] Unknown address in {&__unbuffered_p0_EAX$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:762:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:762:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:765:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:765:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice2, NoOffset)), AddrOf(Var(weak$$choice1, NoOffset)), AddrOf(Var(weak$$choice0, NoOffset)), AddrOf(Var(y, NoOffset)), AddrOf(Var(x$w_buff1_used, NoOffset)), AddrOf(Var(x$w_buff1, NoOffset)), AddrOf(Var(x$w_buff0_used, NoOffset)), AddrOf(Var(x$w_buff0, NoOffset)), AddrOf(Var(x$read_delayed_var, NoOffset)), AddrOf(Var(x$read_delayed, NoOffset)), AddrOf(Var(x$r_buff1_thd3, NoOffset)), AddrOf(Var(x$r_buff1_thd2, NoOffset)), AddrOf(Var(x$r_buff1_thd1, NoOffset)), AddrOf(Var(x$r_buff1_thd0, NoOffset)), AddrOf(Var(x$r_buff0_thd3, NoOffset)), AddrOf(Var(x$r_buff0_thd2, NoOffset)), AddrOf(Var(x$r_buff0_thd1, NoOffset)), AddrOf(Var(x$r_buff0_thd0, NoOffset)), AddrOf(Var(x$mem_tmp, NoOffset)), AddrOf(Var(x$flush_delayed, NoOffset)), AddrOf(Var(x, NoOffset)), AddrOf(Var(main$tmp_guard1, NoOffset)), AddrOf(Var(main$tmp_guard0, NoOffset)), AddrOf(Var(__unbuffered_p1_EBX, NoOffset)), AddrOf(Var(__unbuffered_p1_EAX, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed_var, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$mem_tmp, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$flush_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX, NoOffset)), AddrOf(Var(__unbuffered_cnt, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:765:3)
[Warning][Unknown] Unknown address in {&x$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:765:3)
[Warning][Unknown] Unknown address in {&__unbuffered_p0_EAX$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:765:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:765:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:798:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:798:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice2,
                                     NoOffset)), AddrOf(Var(weak$$choice1, NoOffset)), AddrOf(Var(weak$$choice0, NoOffset)), AddrOf(Var(y, NoOffset)), AddrOf(Var(x$w_buff1_used, NoOffset)), AddrOf(Var(x$w_buff1, NoOffset)), AddrOf(Var(x$w_buff0_used, NoOffset)), AddrOf(Var(x$w_buff0, NoOffset)), AddrOf(Var(x$read_delayed_var, NoOffset)), AddrOf(Var(x$read_delayed, NoOffset)), AddrOf(Var(x$r_buff1_thd3, NoOffset)), AddrOf(Var(x$r_buff1_thd2, NoOffset)), AddrOf(Var(x$r_buff1_thd1, NoOffset)), AddrOf(Var(x$r_buff1_thd0, NoOffset)), AddrOf(Var(x$r_buff0_thd3, NoOffset)), AddrOf(Var(x$r_buff0_thd2, NoOffset)), AddrOf(Var(x$r_buff0_thd1, NoOffset)), AddrOf(Var(x$r_buff0_thd0, NoOffset)), AddrOf(Var(x$mem_tmp, NoOffset)), AddrOf(Var(x$flush_delayed, NoOffset)), AddrOf(Var(x, NoOffset)), AddrOf(Var(main$tmp_guard1, NoOffset)), AddrOf(Var(main$tmp_guard0, NoOffset)), AddrOf(Var(__unbuffered_p1_EBX, NoOffset)), AddrOf(Var(__unbuffered_p1_EAX, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed_var, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$mem_tmp, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$flush_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX, NoOffset)), AddrOf(Var(__unbuffered_cnt, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:798:3)
[Warning][Unknown] Unknown address in {&x$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:798:3)
[Warning][Unknown] Unknown address in {&__unbuffered_p0_EAX$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:798:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:798:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:799:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:799:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice2, NoOffset)), AddrOf(Var(weak$$choice1, NoOffset)), AddrOf(Var(weak$$choice0, NoOffset)), AddrOf(Var(y, NoOffset)), AddrOf(Var(x$w_buff1_used, NoOffset)), AddrOf(Var(x$w_buff1, NoOffset)), AddrOf(Var(x$w_buff0_used, NoOffset)), AddrOf(Var(x$w_buff0, NoOffset)), AddrOf(Var(x$read_delayed_var, NoOffset)), AddrOf(Var(x$read_delayed, NoOffset)), AddrOf(Var(x$r_buff1_thd3, NoOffset)), AddrOf(Var(x$r_buff1_thd2, NoOffset)), AddrOf(Var(x$r_buff1_thd1, NoOffset)), AddrOf(Var(x$r_buff1_thd0, NoOffset)), AddrOf(Var(x$r_buff0_thd3, NoOffset)), AddrOf(Var(x$r_buff0_thd2, NoOffset)), AddrOf(Var(x$r_buff0_thd1, NoOffset)), AddrOf(Var(x$r_buff0_thd0, NoOffset)), AddrOf(Var(x$mem_tmp, NoOffset)), AddrOf(Var(x$flush_delayed, NoOffset)), AddrOf(Var(x, NoOffset)), AddrOf(Var(main$tmp_guard1, NoOffset)), AddrOf(Var(main$tmp_guard0, NoOffset)), AddrOf(Var(__unbuffered_p1_EBX, NoOffset)), AddrOf(Var(__unbuffered_p1_EAX, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed_var, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$mem_tmp, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$flush_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX, NoOffset)), AddrOf(Var(__unbuffered_cnt, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:799:3)
[Warning][Unknown] Unknown address in {&x$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:799:3)
[Warning][Unknown] Unknown address in {&__unbuffered_p0_EAX$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:799:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:799:3)
[Warning][Unknown] Function definition missing for __VERIFIER_nondet_bool (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:866:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:866:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice2,
                                     NoOffset)), AddrOf(Var(weak$$choice1, NoOffset)), AddrOf(Var(weak$$choice0, NoOffset)), AddrOf(Var(y, NoOffset)), AddrOf(Var(x$w_buff1_used, NoOffset)), AddrOf(Var(x$w_buff1, NoOffset)), AddrOf(Var(x$w_buff0_used, NoOffset)), AddrOf(Var(x$w_buff0, NoOffset)), AddrOf(Var(x$read_delayed_var, NoOffset)), AddrOf(Var(x$read_delayed, NoOffset)), AddrOf(Var(x$r_buff1_thd3, NoOffset)), AddrOf(Var(x$r_buff1_thd2, NoOffset)), AddrOf(Var(x$r_buff1_thd1, NoOffset)), AddrOf(Var(x$r_buff1_thd0, NoOffset)), AddrOf(Var(x$r_buff0_thd3, NoOffset)), AddrOf(Var(x$r_buff0_thd2, NoOffset)), AddrOf(Var(x$r_buff0_thd1, NoOffset)), AddrOf(Var(x$r_buff0_thd0, NoOffset)), AddrOf(Var(x$mem_tmp, NoOffset)), AddrOf(Var(x$flush_delayed, NoOffset)), AddrOf(Var(x, NoOffset)), AddrOf(Var(main$tmp_guard1, NoOffset)), AddrOf(Var(main$tmp_guard0, NoOffset)), AddrOf(Var(__unbuffered_p1_EBX, NoOffset)), AddrOf(Var(__unbuffered_p1_EAX, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0_used, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$w_buff0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed_var, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$read_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff1_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd3, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd2, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd1, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$r_buff0_thd0, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$mem_tmp, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX$flush_delayed, NoOffset)), AddrOf(Var(__unbuffered_p0_EAX, NoOffset)), AddrOf(Var(__unbuffered_cnt, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:866:3)
[Warning][Unknown] Unknown address in {&x$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:866:3)
[Warning][Unknown] Unknown address in {&__unbuffered_p0_EAX$read_delayed_var} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:866:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(weak$$choice1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:866:3)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:867:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:867:3)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:86:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:91:1)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:96:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:101:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:106:1)
[Warning][Deadcode] Function "fence" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:837:1)
[Warning][Deadcode] Function "isync" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:840:1)
[Warning][Deadcode] Function "lwfence" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:843:1)
[Warning][Race] Memory location weak$$choice0@rfi006_power.oepc.i:755:7 (race with conf. 110):
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:766:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:769:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:770:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:772:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:761:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:798:3)
[Warning][Race] Memory location x$w_buff1_used@rfi006_power.oepc.i:752:7 (race with conf. 110):
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:766:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:767:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:768:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:769:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:770:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:771:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:772:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:802:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:803:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:804:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:805:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:806:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:807:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:808:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:826:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:828:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:830:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:859:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:861:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:863:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:770:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:806:3)
  write with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:828:3)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:861:3)
[Warning][Race] Memory location x$flush_delayed@rfi006_power.oepc.i:737:7 (race with conf. 110):
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:776:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:810:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:763:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:777:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:800:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:811:3)
[Warning][Race] Memory location x$w_buff0_used@rfi006_power.oepc.i:750:7 (race with conf. 110):
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:766:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:767:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:768:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:769:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:770:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:771:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:772:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:802:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:803:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:804:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:805:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:806:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:807:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:808:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:826:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:827:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:828:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:829:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:830:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:859:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:860:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:861:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:862:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:863:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:769:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:805:3)
  write with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:827:3)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:860:3)
[Warning][Race] Memory location weak$$choice1@rfi006_power.oepc.i:756:7 (race with conf. 110):
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:766:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:769:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:867:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:765:3)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:866:3)
[Warning][Race] Memory location weak$$choice2@rfi006_power.oepc.i:757:7 (race with conf. 110):
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:763:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:767:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:768:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:769:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:770:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:771:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:772:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:800:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:803:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:804:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:805:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:806:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:807:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:808:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:762:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:799:3)
[Warning][Race] Memory location __unbuffered_p0_EAX$read_delayed@rfi006_power.oepc.i:723:7 (race with conf. 110):
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:867:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:773:3)
[Warning][Race] Memory location __unbuffered_p0_EAX$read_delayed_var@rfi006_power.oepc.i:724:5 (race with conf. 110):
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:867:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:774:3)
[Warning][Race] Memory location y@rfi006_power.oepc.i:754:5 (race with conf. 110):
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:795:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:868:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:780:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:792:3)
[Warning][Race] Memory location x$w_buff1@rfi006_power.oepc.i:751:5 (race with conf. 110):
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:766:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:768:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:802:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:804:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:826:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:859:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:768:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:804:3)
[Warning][Race] Memory location __unbuffered_p1_EAX@rfi006_power.oepc.i:730:5 (race with conf. 110):
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:868:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:795:3)
[Warning][Race] Memory location __unbuffered_p1_EBX@rfi006_power.oepc.i:732:5 (race with conf. 110):
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:868:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:809:3)
[Warning][Race] Memory location __unbuffered_p0_EAX@rfi006_power.oepc.i:712:5 (race with conf. 110):
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:867:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:868:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:775:3)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:867:3)
[Warning][Race] Memory location x$mem_tmp@rfi006_power.oepc.i:738:5 (race with conf. 110):
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:776:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:810:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:764:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:801:3)
[Warning][Race] Memory location x$w_buff0@rfi006_power.oepc.i:749:5 (race with conf. 110):
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:766:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:767:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:802:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:803:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:826:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:859:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:767:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:803:3)
[Warning][Race] Memory location x@rfi006_power.oepc.i:736:5 (race with conf. 110):
  read with {thread:([main], {})} (conf. 100) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:867:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:764:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:766:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:775:3)
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:776:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:801:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:802:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:809:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:810:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:826:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:859:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:766:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:776:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:802:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:810:3)
  write with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:823:3)
  write with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:826:3)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:859:3)
[Warning][Race] Memory location __unbuffered_cnt@rfi006_power.oepc.i:710:5 (race with conf. 110):
  read with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:785:3)
  read with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:816:3)
  read with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:833:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:855:3)
  write with {thread:([P0@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:851:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:785:3)
  write with {thread:([P1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:853:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:816:3)
  write with {thread:([P2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:854:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi006_power.oepc.i:833:3)

Summary for all memory locations:
	safe:           10
	vulnerable:      0
	unsafe:         17
	-------------------
	total:          27
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
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-wmm/rfi006_power.oepc.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 780 781 785 786 792 793 795 796 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 816 817 823 824 826 827 828 829 830 831 833 834 855 856 859 860 861 862 863 864 866 867 868 869 
The number of races before goblint filter: 64
The number of races after goblint filter: 0
Race categories: 0
Runtime Symex: 2.87102s
Adding SC constraints
Shared __CPROVER_threads_exited: 3R/4W
Shared __CPROVER_next_thread_id: 2R/4W
Shared __unbuffered_cnt: 4R/4W
Shared __unbuffered_p0_EAX: 1R/3W
Shared __unbuffered_p0_EAX$read_delayed: 1R/2W
Shared __unbuffered_p0_EAX$read_delayed_var: 1R/2W
Shared __unbuffered_p1_EAX: 1R/2W
Shared __unbuffered_p1_EBX: 1R/2W
Shared main$tmp_guard0: 2R/2W
Shared main$tmp_guard1: 2R/2W
Shared x: 4R/6W
Shared x$r_buff0_thd0: 1R/2W
Shared x$r_buff0_thd1: 1R/2W
Shared x$r_buff0_thd2: 1R/2W
Shared x$r_buff0_thd3: 1R/2W
Shared x$r_buff1_thd0: 1R/2W
Shared x$r_buff1_thd1: 1R/2W
Shared x$r_buff1_thd2: 1R/2W
Shared x$r_buff1_thd3: 1R/2W
Shared x$w_buff0: 4R/3W
Shared x$w_buff0_used: 4R/5W
Shared x$w_buff1: 4R/3W
Shared x$w_buff1_used: 4R/5W
Shared y: 2R/3W
Shared __unbuffered_p0_EAX$read_delayed_var$object: 1R/1W
size of program expression: 707 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.00206936s
VERIFICATION SUCCESSFUL
