./goblint --conf conf/svcomp-ghost.json --set ana.base.privatization mutex-meet --set 'ana.activated[+]' apron --set 'ana.autotune.activated[-]' octagon --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] Disabling witness.invariant.all-locals implicitly enables cil.addNestedScopeAttr.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )

[Info] runtime: 00:00:10.118
[Info] vars: 431, evals: 1074

[Info] |called|=136

Memory statistics: total=630.04MB, max=15.81MB, minor=627.85MB, major=18.31MB, promoted=16.11MB
    minor collections=302  major collections=7 compactions=0


[Info] runtime: 00:00:20.146
[Info] vars: 574, evals: 1416

[Info] |called|=144

Memory statistics: total=898.73MB, max=15.81MB, minor=896.53MB, major=21.17MB, promoted=18.96MB
    minor collections=431  major collections=8 compactions=0


[Info] runtime: 00:00:30.166
[Info] vars: 604, evals: 1726

[Info] |called|=130

Memory statistics: total=1279.51MB, max=15.81MB, minor=1277.29MB, major=25.13MB, promoted=22.90MB
    minor collections=613  major collections=9 compactions=0


[Info] runtime: 00:00:40.206
[Info] vars: 610, evals: 2026

[Info] |called|=116

Memory statistics: total=1691.01MB, max=18.18MB, minor=1688.79MB, major=27.84MB, promoted=25.62MB
    minor collections=809  major collections=9 compactions=0


[Info] runtime: 00:00:50.213
[Info] vars: 638, evals: 2390

[Info] |called|=139

Memory statistics: total=1968.86MB, max=18.18MB, minor=1966.63MB, major=30.20MB, promoted=27.97MB
    minor collections=942  major collections=10 compactions=0


[Info] runtime: 00:01:00.230
[Info] vars: 669, evals: 2758

[Info] |called|=135

Memory statistics: total=2243.47MB, max=18.18MB, minor=2241.24MB, major=32.50MB, promoted=30.27MB
    minor collections=1073  major collections=10 compactions=0


[Info] runtime: 00:01:10.249
[Info] vars: 701, evals: 3166

[Info] |called|=137

Memory statistics: total=2515.04MB, max=18.18MB, minor=2512.81MB, major=34.92MB, promoted=32.69MB
    minor collections=1203  major collections=11 compactions=0


[Info] runtime: 00:01:20.259
[Info] vars: 736, evals: 3611

[Info] |called|=136

Memory statistics: total=2788.72MB, max=18.18MB, minor=2786.49MB, major=37.55MB, promoted=35.32MB
    minor collections=1334  major collections=11 compactions=0


[Info] runtime: 00:01:30.289
[Info] vars: 784, evals: 3989

[Info] |called|=108

Memory statistics: total=3153.00MB, max=18.18MB, minor=3150.76MB, major=41.97MB, promoted=39.72MB
    minor collections=1508  major collections=12 compactions=0


[Info] runtime: 00:01:40.314
[Info] vars: 792, evals: 4463

[Info] |called|=133

Memory statistics: total=3604.38MB, max=18.18MB, minor=3602.14MB, major=45.89MB, promoted=43.64MB
    minor collections=1724  major collections=13 compactions=0


[Info] runtime: 00:01:50.325
[Info] vars: 1003, evals: 5390

[Info] |called|=154

Memory statistics: total=4273.63MB, max=20.91MB, minor=4271.37MB, major=53.70MB, promoted=51.44MB
    minor collections=2043  major collections=14 compactions=0


[Info] runtime: 00:02:00.331
[Info] vars: 1059, evals: 5721

[Info] |called|=125

Memory statistics: total=4537.84MB, max=20.91MB, minor=4535.56MB, major=57.79MB, promoted=55.50MB
    minor collections=2170  major collections=15 compactions=0


[Info] runtime: 00:02:10.358
[Info] vars: 1200, evals: 6481

[Info] |called|=132

Memory statistics: total=5065.85MB, max=20.91MB, minor=5063.52MB, major=65.69MB, promoted=63.37MB
    minor collections=2422  major collections=16 compactions=0


[Info] runtime: 00:02:20.379
[Info] vars: 1247, evals: 6957

[Info] |called|=126

Memory statistics: total=5411.43MB, max=24.04MB, minor=5409.09MB, major=71.10MB, promoted=68.77MB
    minor collections=2587  major collections=17 compactions=0


[Info] runtime: 00:02:30.399
[Info] vars: 1248, evals: 7390

[Info] |called|=107

Memory statistics: total=5742.48MB, max=24.04MB, minor=5740.14MB, major=75.00MB, promoted=72.66MB
    minor collections=2745  major collections=17 compactions=0


[Info] runtime: 00:02:40.419
[Info] vars: 1269, evals: 7902

[Info] |called|=88

Memory statistics: total=6111.64MB, max=24.04MB, minor=6109.30MB, major=80.13MB, promoted=77.79MB
    minor collections=2922  major collections=18 compactions=0


[Info] runtime: 00:02:50.426
[Info] vars: 1291, evals: 8460

[Info] |called|=89

Memory statistics: total=6514.14MB, max=24.04MB, minor=6511.79MB, major=84.73MB, promoted=82.38MB
    minor collections=3114  major collections=19 compactions=0


[Info] runtime: 00:03:00.443
[Info] vars: 1312, evals: 9026

[Info] |called|=76

Memory statistics: total=6930.84MB, max=24.04MB, minor=6928.49MB, major=89.04MB, promoted=86.69MB
    minor collections=3313  major collections=19 compactions=0


[Info] runtime: 00:03:10.461
[Info] vars: 1339, evals: 9547

[Info] |called|=59

Memory statistics: total=7324.04MB, max=24.04MB, minor=7321.69MB, major=92.97MB, promoted=90.62MB
    minor collections=3501  major collections=20 compactions=0


[Info] runtime: 00:03:20.489
[Info] vars: 1379, evals: 10095

[Info] |called|=54

Memory statistics: total=7706.34MB, max=24.04MB, minor=7703.98MB, major=98.68MB, promoted=96.32MB
    minor collections=3684  major collections=21 compactions=0


[Info] runtime: 00:03:30.512
[Info] vars: 1510, evals: 10623

[Info] |called|=120

Memory statistics: total=8029.32MB, max=24.04MB, minor=8026.96MB, major=102.62MB, promoted=100.26MB
    minor collections=3838  major collections=21 compactions=0


[Info] runtime: 00:03:40.545
[Info] vars: 1533, evals: 11181

[Info] |called|=103

Memory statistics: total=8423.56MB, max=24.04MB, minor=8421.19MB, major=107.76MB, promoted=105.39MB
    minor collections=4026  major collections=22 compactions=0


[Info] runtime: 00:03:50.557
[Info] vars: 1567, evals: 11780

[Info] |called|=115

Memory statistics: total=8833.63MB, max=24.04MB, minor=8831.26MB, major=113.04MB, promoted=110.67MB
    minor collections=4222  major collections=23 compactions=0


[Info] runtime: 00:04:00.577
[Info] vars: 1569, evals: 12379

[Info] |called|=127

Memory statistics: total=9230.17MB, max=27.65MB, minor=9227.80MB, major=117.15MB, promoted=114.78MB
    minor collections=4411  major collections=23 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)

[Info] runtime: 00:04:10.592
[Info] vars: 1569, evals: 12771

[Info] |called|=0

Memory statistics: total=9637.36MB, max=27.65MB, minor=9634.96MB, major=121.55MB, promoted=119.14MB
    minor collections=4606  major collections=24 compactions=0

[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)

[Info] runtime: 00:04:20.607
[Info] vars: 1569, evals: 12771

[Info] |called|=0

Memory statistics: total=10001.66MB, max=27.65MB, minor=9999.24MB, major=126.23MB, promoted=123.81MB
    minor collections=4780  major collections=25 compactions=0

[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' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:899:3-899:116)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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$w_buff1_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 '! x$r_buff0_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:813:3-813:222)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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-571] condition 'x$r_buff0_thd2' (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 'x$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:837:3-837:104)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd4' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:901:3-901:80)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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 'y$r_buff0_thd4' (possibly inserted by CIL) 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_buff1_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$w_buff1_used' (possibly inserted by CIL) 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 '! x$r_buff0_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:814:3-814: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/mix014_tso.oepc.i:814:3-814:228)
[Warning][Deadcode][CWE-570] condition 'x$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:839:3-839:116)
[Warning][Deadcode][CWE-571] condition 'x$r_buff0_thd2' (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' (possibly inserted by CIL) 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' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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 '0' 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' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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$w_buff1_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$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:841:3-841:116)
[Warning][Deadcode][CWE-570] condition '! x$r_buff0_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:815:3-815: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/mix014_tso.oepc.i:815:3-815:222)
[Warning][Deadcode][CWE-571] condition 'x$r_buff0_thd2' (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-571] condition 'y$w_buff0_used' (possibly inserted by CIL) 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' (possibly inserted by CIL) 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_thd0' (possibly inserted by CIL) 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_buff0_thd1' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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 '! y$r_buff0_thd2' (possibly inserted by CIL) 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' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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_thd1' (possibly inserted by CIL) 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' (possibly inserted by CIL) 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_thd0' (possibly inserted by CIL) 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_thd1' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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_thd0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:938:3-938:80)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd1' (possibly inserted by CIL) 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' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:868:3-868:80)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd2' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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' (possibly inserted by CIL) 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 'x$r_buff0_thd1' (possibly inserted by CIL) 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' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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 'x$w_buff1_used' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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 'y$r_buff0_thd0' (possibly inserted by CIL) 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 'x$r_buff0_thd3' (possibly inserted by CIL) 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 'y$w_buff1_used' (possibly inserted by CIL) 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 'x$r_buff0_thd3' (possibly inserted by CIL) 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 '! y$r_buff0_thd2' (possibly inserted by CIL) 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 'x$w_buff1_used' (possibly inserted by CIL) 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 '! y$w_buff1_used' (possibly inserted by CIL) 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 'x$w_buff0_used' (possibly inserted by CIL) 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 'y$r_buff0_thd0' (possibly inserted by CIL) 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_thd3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:872:3-872:104)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:872:3-872:104)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' (possibly inserted by CIL) 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_thd3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:873:3-873:80)
[Warning][Deadcode][CWE-571] condition '! x$w_buff1_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 '! y$r_buff0_thd2' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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 '! x$r_buff0_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:809:3-809:163)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:944:3-944:116)
[Warning][Deadcode][CWE-570] condition 'y$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:874:3-874:116)
[Warning][Deadcode][CWE-570] condition 'y$w_buff1_used' (possibly inserted by CIL) 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$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-570] condition 'y$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:874:3-874:116)
[Warning][Deadcode][CWE-571] condition 'x$r_buff0_thd2' (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-570] condition 'y$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:875:3-875:80)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:951:3-951:163)
[Warning][Deadcode][CWE-570] condition 'y$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:876:3-876:116)
[Warning][Deadcode][CWE-571] condition '! x$w_buff1_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-571] condition '! x$w_buff1_used' (possibly inserted by CIL) 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' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:829:3-829:222)
[Warning][Deadcode][CWE-570] condition '! x$r_buff0_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:810:3-810:209)
[Warning][Deadcode][CWE-570] condition 'y$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:876:3-876:116)
[Warning][Deadcode][CWE-571] condition '! y$w_buff1_used' (possibly inserted by CIL) 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$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-571] condition 'x$r_buff0_thd2' (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-571] condition '! x$r_buff0_thd0' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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$w_buff1_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-571] condition '! y$r_buff0_thd2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:830:3-830:228)
[Warning][Deadcode][CWE-570] condition '! x$r_buff0_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:811:3-811:209)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd4' (possibly inserted by CIL) 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 '! y$w_buff1_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:830:3-830:228)
[Warning][Deadcode][CWE-570] condition 'x$w_buff1_used' (possibly inserted by CIL) 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-571] condition 'x$r_buff0_thd2' (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_buff0_thd4' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:896:3-896:80)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd0' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:953:3-953:209)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd4' (possibly inserted by CIL) 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_buff1_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$w_buff1_used' (possibly inserted by CIL) 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 '! y$r_buff0_thd2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:831:3-831:222)
[Warning][Deadcode][CWE-570] condition '! x$r_buff0_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:812:3-812:228)
[Warning][Deadcode][CWE-571] condition '! y$w_buff1_used' (possibly inserted by CIL) 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$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-571] condition 'x$r_buff0_thd2' (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' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix014_tso.oepc.i:898:3-898:80)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 2
[Info][Race] Memory locations race summary:
  safe: 46
  vulnerable: 0
  unsafe: 0
  total memory locations: 46
