./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-data-race.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
Collected factors:
functions: 45
functionCalls: 85
loops: 6
loopBreaks: 0
controlFlowStatements: 664
expressions: 1644
instructions: 460
integralVars: (60,108)
arrayVars: (2,0)
pointerVars: (2,16)

Complexity estimates:
File: 6338
Total: 30251
Congruence: 6809
Enabled congruence domain.
Octagon: 6000
Enabled octagon domain for:
y$w_buff0_used, z$w_buff0_used, i, key, count, a___0, tmp, j, count, k, size, a___0, b, c, i, tmp, tmp___0, tmp___1, tmp___2, tmp___3, tmp___4, tmp___5, tmp___6, tmp, tmp___0, tmp___1, tmp___2, tmp___3, tmp___4, tmp___5, tmp___7, tmp, tmp___0, tmp___1, tmp___2, tmp___3, tmp___4, tmp___5, tmp___7, tmp, __x, __x, __x
Widening: 11104
Enabled widening thresholds
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )

runtime: 00:00:10.117
vars: 1500, evals: 6928

|rho|=1500
|stable|=1079
|infl|=1436
|wpoint|=14
|sides|=481
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=859
|called|=135
Found 88 contexts for 9 functions. Top 5 functions:
40	contexts for L:entry state of __VERIFIER_nondet_bool (315) on lib/sv-comp/stub/src/sv-comp.c:19:63-19:149
22	contexts for L:entry state of __VERIFIER_assert (346) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:18:1-18:104
20	contexts for L:entry state of reach_error (344) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:17:1-17:168
1	contexts for L:entry state of assume_abort_if_not (310) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:2:1-4:1
1	contexts for L:entry state of P2 (1073) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:802:1-860:1

Memory statistics: total=5206.60MB, max=31.05MB, minor=5203.30MB, major=80.74MB, promoted=77.45MB
    minor collections=2488  major collections=15 compactions=0


runtime: 00:00:20.138
vars: 1682, evals: 10268

|rho|=1682
|stable|=1514
|infl|=1635
|wpoint|=14
|sides|=526
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=964
|called|=123
Found 116 contexts for 9 functions. Top 5 functions:
54	contexts for L:entry state of __VERIFIER_nondet_bool (315) on lib/sv-comp/stub/src/sv-comp.c:19:63-19:149
29	contexts for L:entry state of __VERIFIER_assert (346) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:18:1-18:104
27	contexts for L:entry state of reach_error (344) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:17:1-17:168
1	contexts for L:entry state of assume_abort_if_not (310) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:2:1-4:1
1	contexts for L:entry state of P2 (1073) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:802:1-860:1

Memory statistics: total=8178.76MB, max=31.05MB, minor=8175.32MB, major=122.81MB, promoted=119.37MB
    minor collections=3907  major collections=19 compactions=0


runtime: 00:00:30.152
vars: 1914, evals: 12913

|rho|=1914
|stable|=1447
|infl|=1907
|wpoint|=14
|sides|=599
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=1097
|called|=87
Found 130 contexts for 9 functions. Top 5 functions:
62	contexts for L:entry state of __VERIFIER_nondet_bool (315) on lib/sv-comp/stub/src/sv-comp.c:19:63-19:149
32	contexts for L:entry state of __VERIFIER_assert (346) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:18:1-18:104
30	contexts for L:entry state of reach_error (344) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:17:1-17:168
1	contexts for L:entry state of assume_abort_if_not (310) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:2:1-4:1
1	contexts for L:entry state of P2 (1073) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:802:1-860:1

Memory statistics: total=10625.71MB, max=35.71MB, minor=10622.18MB, major=157.01MB, promoted=153.49MB
    minor collections=5076  major collections=23 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:778:3-778:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:798:3-798:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:857:3-857:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:908:3-908:42)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:85:1-89:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:90:1-94:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:95:1-99:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:100:1-104:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:105:1-109:1)
[Warning][Deadcode] Function 'fence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:912:1-914:1)
[Warning][Deadcode] Function 'isync' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:915:1-917:1)
[Warning][Deadcode] Function 'lwfence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:918:1-920:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 182
  dead: 8 (8 in uncalled functions)
  total lines: 190
[Warning][Deadcode][CWE-571] condition 'y$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:825:3-825:228)
[Warning][Deadcode][CWE-571] condition 'z$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:887:3-887:222)
[Warning][Deadcode][CWE-571] condition 'y$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:826:3-826:222)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:896:3-896:104)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:896:3-896:104)
[Warning][Deadcode][CWE-571] condition 'y$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:827:3-827:228)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:897:3-897:80)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:898:3-898:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:898:3-898:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:899:3-899:80)
[Warning][Deadcode][CWE-571] condition 'y$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:828:3-828:222)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:900:3-900:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:900:3-900:116)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:838:3-838:163)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:838:3-838:163)
[Warning][Deadcode][CWE-571] condition '! z$r_buff1_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:838:3-838:163)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:839:3-839:209)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:839:3-839:209)
[Warning][Deadcode][CWE-571] condition '! z$r_buff1_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:839:3-839:209)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:840:3-840:209)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:840:3-840:209)
[Warning][Deadcode][CWE-571] condition '! z$r_buff1_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:840:3-840:209)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:936:3-936:104)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:936:3-936:104)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:937:3-937:80)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:841:3-841:228)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:938:3-938:116)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:841:3-841:228)
[Warning][Deadcode][CWE-571] condition '! z$r_buff1_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:841:3-841:228)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:938:3-938:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:939:3-939:80)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:940:3-940:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:940:3-940:116)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:842:3-842:222)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:842:3-842:222)
[Warning][Deadcode][CWE-571] condition '! z$r_buff1_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:842:3-842:222)
[Warning][Deadcode][CWE-570] condition 'z$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:941:3-941:104)
[Warning][Deadcode][CWE-570] condition 'z$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:941:3-941:104)
[Warning][Deadcode][CWE-570] condition 'z$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:942:3-942:80)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:843:3-843:228)
[Warning][Deadcode][CWE-570] condition 'z$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:943:3-943:116)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:843:3-843:228)
[Warning][Deadcode][CWE-571] condition '! z$r_buff1_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:843:3-843:228)
[Warning][Deadcode][CWE-570] condition 'z$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:943:3-943:116)
[Warning][Deadcode][CWE-570] condition 'z$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:944:3-944:80)
[Warning][Deadcode][CWE-570] condition 'z$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:945:3-945:116)
[Warning][Deadcode][CWE-570] condition 'z$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:945:3-945:116)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:844:3-844:222)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:844:3-844:222)
[Warning][Deadcode][CWE-571] condition '! z$r_buff1_thd3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:844:3-844:222)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:952:3-952:163)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:952:3-952:163)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:952:3-952:163)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:953:3-953:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:953:3-953:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:953:3-953:209)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:17:73-17:74)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:954:3-954:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:954:3-954:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:954:3-954:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:955:3-955:228)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:955:3-955:228)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:955:3-955:228)
[Warning][Deadcode][CWE-571] condition 'z$w_buff0_used' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:868:3-868:57)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:791:3-791:104)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:791:3-791:104)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:792:3-792:80)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:956:3-956:222)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:793:3-793:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:956:3-956:222)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:956:3-956:222)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:793:3-793:116)
[Warning][Deadcode][CWE-571] condition 'z$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:881:3-881:163)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:794:3-794:80)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:795:3-795:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:957:3-957:228)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:795:3-795:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:957:3-957:228)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:957:3-957:228)
[Warning][Deadcode][CWE-571] condition 'z$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:882:3-882:209)
[Warning][Deadcode][CWE-571] condition 'y$w_buff0_used' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:809:3-809:57)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:958:3-958:222)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:958:3-958:222)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:958:3-958:222)
[Warning][Deadcode][CWE-571] condition 'z$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:883:3-883:209)
[Warning][Deadcode][CWE-571] condition 'y$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:822:3-822:163)
[Warning][Deadcode][CWE-571] condition 'z$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:884:3-884:228)
[Warning][Deadcode][CWE-571] condition 'y$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:823:3-823:209)
[Warning][Deadcode][CWE-571] condition 'z$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:885:3-885:222)
[Warning][Deadcode][CWE-571] condition 'y$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:824:3-824:209)
[Warning][Deadcode][CWE-571] condition 'z$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:886:3-886:228)
SV-COMP result: true
[Info][Race] Memory locations race summary:
  safe: 45
  vulnerable: 0
  unsafe: 0
  total memory locations: 45
