./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/mix006_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: 44
functionCalls: 76
loops: 6
loopBreaks: 0
controlFlowStatements: 661
expressions: 1612
instructions: 446
integralVars: (54,107)
arrayVars: (2,0)
pointerVars: (2,15)

Complexity estimates:
File: 6142
Total: 30226
Congruence: 6337
Enabled congruence domain.
Octagon: 6000
Enabled octagon domain for:
x$w_buff0_used, y$w_buff0_used, i, key, count, a, tmp, j, count, k, size, a, 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: 11747
Enabled widening thresholds
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )

runtime: 00:00:10.098
vars: 1460, evals: 6768

|rho|=1460
|stable|=1053
|infl|=1397
|wpoint|=14
|sides|=461
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=842
|called|=132
Found 87 contexts for 8 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/mix006_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/mix006_tso.oepc.i:17:1-17:168
1	contexts for L:entry state of P0 (1067) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:760:1-779:1
1	contexts for L:entry state of P1 (1070) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:780:1-837:1

Memory statistics: total=5132.83MB, max=31.05MB, minor=5129.54MB, major=79.18MB, promoted=75.89MB
    minor collections=2453  major collections=15 compactions=0


runtime: 00:00:20.120
vars: 1642, evals: 10080

|rho|=1642
|stable|=1520
|infl|=1596
|wpoint|=14
|sides|=506
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=947
|called|=66
Found 115 contexts for 8 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/mix006_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/mix006_tso.oepc.i:17:1-17:168
1	contexts for L:entry state of P0 (1067) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:760:1-779:1
1	contexts for L:entry state of P1 (1070) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:780:1-837:1

Memory statistics: total=8143.80MB, max=31.05MB, minor=8140.34MB, major=121.95MB, promoted=118.49MB
    minor collections=3891  major collections=19 compactions=0


runtime: 00:00:30.136
vars: 1893, evals: 12751

|rho|=1893
|stable|=1533
|infl|=1886
|wpoint|=14
|sides|=582
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=1093
|called|=128
Found 133 contexts for 8 functions. Top 5 functions:
64	contexts for L:entry state of __VERIFIER_nondet_bool (315) on lib/sv-comp/stub/src/sv-comp.c:19:63-19:149
33	contexts for L:entry state of __VERIFIER_assert (346) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:18:1-18:104
31	contexts for L:entry state of reach_error (344) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:17:1-17:168
1	contexts for L:entry state of P0 (1067) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:760:1-779:1
1	contexts for L:entry state of P1 (1070) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:780:1-837:1

Memory statistics: total=10522.15MB, max=35.71MB, minor=10518.59MB, major=155.42MB, promoted=151.86MB
    minor collections=5027  major collections=23 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:776:3-776:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:834:3-834:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:884:3-884:42)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_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/mix006_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/mix006_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/mix006_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/mix006_tso.oepc.i:105:1-109:1)
[Warning][Deadcode] Function 'fence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:888:1-890:1)
[Warning][Deadcode] Function 'isync' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:891:1-893:1)
[Warning][Deadcode] Function 'lwfence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:894:1-896:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 166
  dead: 8 (8 in uncalled functions)
  total lines: 174
[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/mix006_tso.oepc.i:863:3-863:222)
[Warning][Deadcode][CWE-571] condition 'x$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:803:3-803:222)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:872:3-872:104)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:872:3-872:104)
[Warning][Deadcode][CWE-571] condition 'x$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:804:3-804:228)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:873:3-873:80)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:874:3-874:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:874:3-874:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:875:3-875:80)
[Warning][Deadcode][CWE-571] condition 'x$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:805:3-805:222)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:876:3-876:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:876:3-876:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:815:3-815:163)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:815:3-815:163)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:815:3-815:163)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:816:3-816:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:816:3-816:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:816:3-816:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:817:3-817:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:817:3-817:209)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:910:3-910:104)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:817:3-817:209)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:910:3-910:104)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:911:3-911:80)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:818:3-818:228)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:912:3-912:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:818:3-818:228)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:912:3-912:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:818:3-818:228)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:913:3-913:80)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:914:3-914:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:914:3-914:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:819:3-819:222)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:819:3-819:222)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:915:3-915:104)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:819:3-819:222)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:915:3-915:104)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:916:3-916:80)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:820:3-820:228)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:917:3-917:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:820:3-820:228)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:917:3-917:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:820:3-820:228)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:918:3-918:80)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:919:3-919:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:919:3-919:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:821:3-821:222)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:821:3-821:222)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:821:3-821:222)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:926:3-926:163)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:926:3-926:163)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:926:3-926:163)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:927:3-927:209)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:927:3-927:209)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:927:3-927:209)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:928:3-928:209)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:928:3-928:209)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:928:3-928:209)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:17:73-17:74)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:929:3-929:228)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:929:3-929:228)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:929:3-929:228)
[Warning][Deadcode][CWE-571] condition 'y$w_buff0_used' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:845:3-845:57)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:769:3-769:104)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:769:3-769:104)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:770:3-770:80)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:930:3-930:222)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:930:3-930:222)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:930:3-930:222)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:771:3-771:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:771:3-771:116)
[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/mix006_tso.oepc.i:857:3-857:163)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:772:3-772:80)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:773:3-773:116)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:931:3-931:228)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:773:3-773:116)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:931:3-931:228)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:931:3-931: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/mix006_tso.oepc.i:858:3-858:209)
[Warning][Deadcode][CWE-571] condition 'x$w_buff0_used' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:787:3-787:57)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:932:3-932:222)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:932:3-932:222)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:932:3-932: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/mix006_tso.oepc.i:859:3-859:209)
[Warning][Deadcode][CWE-571] condition 'x$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:799:3-799:163)
[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/mix006_tso.oepc.i:860:3-860:228)
[Warning][Deadcode][CWE-571] condition 'x$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:800:3-800: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/mix006_tso.oepc.i:861:3-861:222)
[Warning][Deadcode][CWE-571] condition 'x$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:801:3-801: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/mix006_tso.oepc.i:862:3-862:228)
[Warning][Deadcode][CWE-571] condition 'x$w_buff0_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:802:3-802:228)
SV-COMP result: true
[Info][Race] Memory locations race summary:
  safe: 40
  vulnerable: 0
  unsafe: 0
  total memory locations: 40
