./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/mix014_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: 83
loops: 6
loopBreaks: 0
controlFlowStatements: 625
expressions: 1554
instructions: 435
integralVars: (62,97)
arrayVars: (2,0)
pointerVars: (2,16)

Complexity estimates:
File: 5527
Total: 28146
Congruence: 6139
Enabled congruence domain.
Octagon: 6000
Enabled octagon domain for:
x$w_buff0_used, y$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, tmp___0, tmp___1, tmp, tmp___0, tmp___1, tmp___2, tmp___3, tmp___4, tmp___5, tmp___7, tmp, __x, __x, __x
Widening: 10480
Enabled widening thresholds
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )

runtime: 00:00:10.104
vars: 1363, evals: 6480

|rho|=1363
|stable|=1214
|infl|=1294
|wpoint|=18
|sides|=440
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=785
|called|=76
Found 75 contexts for 8 functions. Top 5 functions:
26	contexts for L:entry state of __VERIFIER_nondet_bool (315) on lib/sv-comp/stub/src/sv-comp.c:19:63-19:149
23	contexts for L:entry state of __VERIFIER_assert (346) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:18:1-18:104
21	contexts for L:entry state of reach_error (344) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_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/mix014_tso.oepc.i:769:1-788:1
1	contexts for L:entry state of P1 (1070) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:789:1-847:1

Memory statistics: total=4818.11MB, max=27.00MB, minor=4814.79MB, major=74.83MB, promoted=71.51MB
    minor collections=2303  major collections=15 compactions=0


runtime: 00:00:20.113
vars: 1501, evals: 9327

|rho|=1501
|stable|=1121
|infl|=1452
|wpoint|=18
|sides|=480
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=863
|called|=127
Found 92 contexts for 9 functions. Top 5 functions:
32	contexts for L:entry state of __VERIFIER_nondet_bool (315) on lib/sv-comp/stub/src/sv-comp.c:19:63-19:149
28	contexts for L:entry state of __VERIFIER_assert (346) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:18:1-18:104
26	contexts for L:entry state of reach_error (344) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_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/mix014_tso.oepc.i:769:1-788:1
1	contexts for L:entry state of assume_abort_if_not (310) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:2:1-4:1

Memory statistics: total=7275.22MB, max=31.05MB, minor=7271.78MB, major=108.79MB, promoted=105.35MB
    minor collections=3477  major collections=19 compactions=0


runtime: 00:00:30.140
vars: 1742, evals: 11720

|rho|=1742
|stable|=1194
|infl|=1735
|wpoint|=18
|sides|=554
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=1002
|called|=137
Found 106 contexts for 9 functions. Top 5 functions:
38	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/mix014_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/mix014_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/mix014_tso.oepc.i:769:1-788:1
1	contexts for L:entry state of assume_abort_if_not (310) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:2:1-4:1

Memory statistics: total=9394.73MB, max=31.05MB, minor=9391.17MB, major=139.06MB, promoted=135.50MB
    minor collections=4489  major collections=22 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:785:3-785:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:844:3-844:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:879:3-879:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:907:3-907:42)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_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/mix014_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/mix014_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/mix014_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/mix014_tso.oepc.i:105:1-109:1)
[Warning][Deadcode] Function 'fence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:911:1-913:1)
[Warning][Deadcode] Function 'isync' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:914:1-916:1)
[Warning][Deadcode] Function 'lwfence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:917:1-919:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 179
  dead: 8 (8 in uncalled functions)
  total lines: 187
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:899:3-899:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:899:3-899:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:900:3-900: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/mix014_tso.oepc.i:813:3-813:222)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:900:3-900:104)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:901:3-901:80)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:902:3-902:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:902:3-902:116)
[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/mix014_tso.oepc.i:814:3-814:228)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:903:3-903:80)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:904:3-904:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:904:3-904:116)
[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/mix014_tso.oepc.i:815:3-815:222)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:935:3-935:104)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:935:3-935:104)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:825:3-825:163)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:936:3-936:80)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:825:3-825:163)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:825:3-825:163)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:937:3-937:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:937:3-937:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:938:3-938:80)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:826:3-826:209)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:939:3-939:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:826:3-826:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:826:3-826:209)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:939:3-939:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:940:3-940:104)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:940:3-940:104)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:827:3-827:209)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:941:3-941:80)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:827:3-827:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:827:3-827:209)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:942:3-942:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:942:3-942:116)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:943:3-943:80)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:828:3-828:228)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:944:3-944:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:828:3-828:228)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:828:3-828:228)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:944:3-944:116)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:951:3-951:163)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:829:3-829:222)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:951:3-951:163)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:951:3-951:163)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:829:3-829:222)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:829:3-829:222)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:952:3-952:209)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:952:3-952:209)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:952:3-952:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:830:3-830:228)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:830:3-830:228)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:830:3-830:228)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:953:3-953:209)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:953:3-953:209)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:953:3-953:209)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:831:3-831:222)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:831:3-831:222)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:831:3-831:222)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:954:3-954:228)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:954:3-954:228)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:954:3-954:228)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:955:3-955:222)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:955:3-955:222)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:955:3-955:222)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_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/mix014_tso.oepc.i:956:3-956:228)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:956:3-956:228)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:956:3-956:228)
[Warning][Deadcode][CWE-571] condition 'y$w_buff0_used' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:855:3-855:57)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:957:3-957:222)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:778:3-778:104)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:957:3-957:222)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:957:3-957:222)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:778:3-778:104)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:779:3-779:80)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:867:3-867:104)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:780:3-780:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:867:3-867:104)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:780:3-780:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:781:3-781:80)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:868:3-868:80)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:782:3-782:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:869:3-869:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:782:3-782:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:869:3-869:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:870:3-870:80)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:871:3-871:116)
[Warning][Deadcode][CWE-571] condition 'x$w_buff0_used' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:796:3-796:57)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:871:3-871:116)
[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/mix014_tso.oepc.i:809:3-809:163)
[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/mix014_tso.oepc.i:810:3-810:209)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:895:3-895: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/mix014_tso.oepc.i:811:3-811:209)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:895:3-895:104)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:896:3-896:80)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:897:3-897:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:897:3-897:116)
[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/mix014_tso.oepc.i:812:3-812:228)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:898:3-898:80)
SV-COMP result: true
[Info][Race] Memory locations race summary:
  safe: 46
  vulnerable: 0
  unsafe: 0
  total memory locations: 46
