./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/mix008_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.128
[Info] vars: 503, evals: 956

[Info] |called|=129

Memory statistics: total=672.26MB, max=15.81MB, minor=670.07MB, major=19.56MB, promoted=17.37MB
    minor collections=323  major collections=7 compactions=0


[Info] runtime: 00:00:20.147
[Info] vars: 599, evals: 1300

[Info] |called|=133

Memory statistics: total=951.15MB, max=15.81MB, minor=948.94MB, major=22.62MB, promoted=20.41MB
    minor collections=456  major collections=8 compactions=0


[Info] runtime: 00:00:30.170
[Info] vars: 621, evals: 1613

[Info] |called|=113

Memory statistics: total=1383.83MB, max=15.81MB, minor=1381.61MB, major=26.48MB, promoted=24.25MB
    minor collections=663  major collections=9 compactions=0


[Info] runtime: 00:00:40.190
[Info] vars: 633, evals: 1959

[Info] |called|=138

Memory statistics: total=1756.01MB, max=18.18MB, minor=1753.78MB, major=29.25MB, promoted=27.02MB
    minor collections=840  major collections=9 compactions=0


[Info] runtime: 00:00:50.198
[Info] vars: 655, evals: 2291

[Info] |called|=126

Memory statistics: total=2092.54MB, max=18.18MB, minor=2090.31MB, major=31.74MB, promoted=29.51MB
    minor collections=1001  major collections=10 compactions=0


[Info] runtime: 00:01:00.216
[Info] vars: 686, evals: 2665

[Info] |called|=113

Memory statistics: total=2381.85MB, max=18.18MB, minor=2379.62MB, major=34.13MB, promoted=31.90MB
    minor collections=1139  major collections=10 compactions=0


[Info] runtime: 00:01:10.222
[Info] vars: 718, evals: 3075

[Info] |called|=114

Memory statistics: total=2656.06MB, max=18.18MB, minor=2653.83MB, major=36.52MB, promoted=34.29MB
    minor collections=1270  major collections=11 compactions=0


[Info] runtime: 00:01:20.229
[Info] vars: 753, evals: 3525

[Info] |called|=122

Memory statistics: total=2926.65MB, max=18.18MB, minor=2924.41MB, major=39.47MB, promoted=37.24MB
    minor collections=1399  major collections=11 compactions=0


[Info] runtime: 00:01:30.244
[Info] vars: 788, evals: 4035

[Info] |called|=134

Memory statistics: total=3260.40MB, max=18.18MB, minor=3258.16MB, major=43.60MB, promoted=41.36MB
    minor collections=1559  major collections=12 compactions=0


[Info] runtime: 00:01:40.256
[Info] vars: 1027, evals: 4558

[Info] |called|=124

Memory statistics: total=3616.75MB, max=18.18MB, minor=3614.48MB, major=47.73MB, promoted=45.47MB
    minor collections=1730  major collections=13 compactions=0


[Info] runtime: 00:01:50.282
[Info] vars: 1124, evals: 5102

[Info] |called|=123

Memory statistics: total=4211.30MB, max=20.91MB, minor=4209.02MB, major=53.39MB, promoted=51.11MB
    minor collections=2014  major collections=14 compactions=0


[Info] runtime: 00:02:00.304
[Info] vars: 1220, evals: 5629

[Info] |called|=94

Memory statistics: total=4722.69MB, max=20.91MB, minor=4720.39MB, major=59.24MB, promoted=56.94MB
    minor collections=2258  major collections=15 compactions=0


[Info] runtime: 00:02:10.340
[Info] vars: 1256, evals: 6131

[Info] |called|=104

Memory statistics: total=5152.37MB, max=24.04MB, minor=5150.05MB, major=64.30MB, promoted=61.98MB
    minor collections=2463  major collections=16 compactions=0


[Info] runtime: 00:02:20.367
[Info] vars: 1300, evals: 6627

[Info] |called|=118

Memory statistics: total=5516.83MB, max=24.04MB, minor=5514.49MB, major=69.93MB, promoted=67.60MB
    minor collections=2637  major collections=16 compactions=0


[Info] runtime: 00:02:30.382
[Info] vars: 1301, evals: 7100

[Info] |called|=124

Memory statistics: total=5891.49MB, max=24.04MB, minor=5889.15MB, major=73.97MB, promoted=71.63MB
    minor collections=2816  major collections=17 compactions=0


[Info] runtime: 00:02:40.394
[Info] vars: 1343, evals: 7600

[Info] |called|=129

Memory statistics: total=6277.81MB, max=24.04MB, minor=6275.47MB, major=79.34MB, promoted=76.99MB
    minor collections=3001  major collections=18 compactions=0


[Info] runtime: 00:02:50.413
[Info] vars: 1352, evals: 8026

[Info] |called|=86

Memory statistics: total=6662.61MB, max=27.65MB, minor=6660.26MB, major=83.74MB, promoted=81.39MB
    minor collections=3184  major collections=18 compactions=0


[Info] runtime: 00:03:00.423
[Info] vars: 1373, evals: 8522

[Info] |called|=105

Memory statistics: total=7073.00MB, max=27.65MB, minor=7070.65MB, major=87.85MB, promoted=85.50MB
    minor collections=3381  major collections=19 compactions=0


[Info] runtime: 00:03:10.439
[Info] vars: 1400, evals: 9032

[Info] |called|=126

Memory statistics: total=7482.99MB, max=27.65MB, minor=7480.64MB, major=91.76MB, promoted=89.41MB
    minor collections=3576  major collections=19 compactions=0


[Info] runtime: 00:03:20.445
[Info] vars: 1427, evals: 9567

[Info] |called|=133

Memory statistics: total=7898.22MB, max=27.65MB, minor=7895.87MB, major=96.08MB, promoted=93.73MB
    minor collections=3775  major collections=20 compactions=0


[Info] runtime: 00:03:30.478
[Info] vars: 1489, evals: 9966

[Info] |called|=26

Memory statistics: total=8284.55MB, max=27.65MB, minor=8282.19MB, major=101.58MB, promoted=99.22MB
    minor collections=3959  major collections=21 compactions=0


[Info] runtime: 00:03:40.494
[Info] vars: 1579, evals: 10531

[Info] |called|=124

Memory statistics: total=8651.37MB, max=27.65MB, minor=8649.01MB, major=105.43MB, promoted=103.07MB
    minor collections=4134  major collections=21 compactions=0


[Info] runtime: 00:03:50.508
[Info] vars: 1602, evals: 11047

[Info] |called|=108

Memory statistics: total=9050.42MB, max=27.65MB, minor=9048.05MB, major=110.21MB, promoted=107.85MB
    minor collections=4325  major collections=22 compactions=0


[Info] runtime: 00:04:00.527
[Info] vars: 1644, evals: 11663

[Info] |called|=134

Memory statistics: total=9479.86MB, max=27.65MB, minor=9477.48MB, major=116.44MB, promoted=114.07MB
    minor collections=4530  major collections=23 compactions=0


[Info] runtime: 00:04:10.534
[Info] vars: 1644, evals: 12030

[Info] |called|=30

Memory statistics: total=9862.34MB, max=27.65MB, minor=9859.96MB, major=119.67MB, promoted=117.29MB
    minor collections=4713  major collections=23 compactions=0


[Info] runtime: 00:04:20.562
[Info] vars: 1646, evals: 12606

[Info] |called|=121

Memory statistics: total=10221.19MB, max=27.65MB, minor=10218.82MB, major=123.03MB, promoted=120.66MB
    minor collections=4884  major collections=24 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)

[Info] runtime: 00:04:30.579
[Info] vars: 1646, evals: 12790

[Info] |called|=0

Memory statistics: total=10632.82MB, max=27.65MB, minor=10630.41MB, major=127.41MB, promoted=125.00MB
    minor collections=5081  major collections=24 compactions=0

[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_buff1_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-570] condition 'z$w_buff1_used' (possibly inserted by CIL) 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' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:844:3-844:222)
[Warning][Deadcode][CWE-570] condition '! y$r_buff0_thd3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:825:3-825:228)
[Warning][Deadcode][CWE-571] condition '! z$w_buff1_used' (possibly inserted by CIL) 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$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 'y$r_buff0_thd3' (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_buff1_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-570] condition '! z$r_buff0_thd4' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:887:3-887:222)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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 '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 'z$r_buff0_thd4' (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_buff1_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_thd3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:826:3-826: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-571] condition 'y$r_buff0_thd3' (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$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:850:3-850:104)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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 'y$r_buff0_thd4' (possibly inserted by CIL) 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_buff1_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$w_buff1_used' (possibly inserted by CIL) 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_buff0_thd3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:827:3-827: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:827:3-827:228)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:17:73-17:74)
[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/mix008_tso.oepc.i:852:3-852:116)
[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/mix008_tso.oepc.i:827:3-827: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/mix008_tso.oepc.i:897:3-897:80)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:954:3-954:209)
[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/mix008_tso.oepc.i:898:3-898: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/mix008_tso.oepc.i:898:3-898: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/mix008_tso.oepc.i:828:3-828:222)
[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/mix008_tso.oepc.i:854:3-854:116)
[Warning][Deadcode][CWE-570] condition '! y$r_buff0_thd3' (possibly inserted by CIL) is always false (/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' (possibly inserted by CIL) 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-571] condition 'y$r_buff0_thd3' (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' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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 '! y$r_buff0_thd0' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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' (possibly inserted by CIL) 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' (possibly inserted by CIL) 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 'z$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:901:3-901: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/mix008_tso.oepc.i:791:3-791:104)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:838:3-838:163)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd2' (possibly inserted by CIL) 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' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:793:3-793:116)
[Warning][Deadcode][CWE-570] condition 'z$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:903:3-903:116)
[Warning][Deadcode][CWE-571] condition '! z$w_buff1_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$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:793:3-793:116)
[Warning][Deadcode][CWE-570] condition '! z$r_buff0_thd4' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:881:3-881: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:881:3-881:163)
[Warning][Deadcode][CWE-571] condition 'z$r_buff0_thd4' (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' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:794:3-794:80)
[Warning][Deadcode][CWE-571] condition '! z$r_buff0_thd3' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:839:3-839:209)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:795:3-795:116)
[Warning][Deadcode][CWE-570] condition 'z$w_buff1_used' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:905:3-905: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/mix008_tso.oepc.i:795:3-795:116)
[Warning][Deadcode][CWE-571] condition '! y$r_buff0_thd0' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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_buff1_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-570] condition '! z$r_buff0_thd4' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:882:3-882: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:882:3-882:209)
[Warning][Deadcode][CWE-571] condition 'z$r_buff0_thd4' (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 '! z$r_buff0_thd3' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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 'y$w_buff0_used' (possibly inserted by CIL) 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' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:958:3-958:222)
[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/mix008_tso.oepc.i:936:3-936: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/mix008_tso.oepc.i:958:3-958:222)
[Warning][Deadcode][CWE-571] condition '! z$w_buff1_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-570] condition 'y$w_buff1_used' (possibly inserted by CIL) 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 '! z$r_buff0_thd4' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:883:3-883: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:883:3-883:209)
[Warning][Deadcode][CWE-571] condition 'z$r_buff0_thd4' (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-570] condition 'y$r_buff0_thd0' (possibly inserted by CIL) 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 '! y$w_buff1_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$r_buff0_thd3' (possibly inserted by CIL) 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$w_buff1_used' (possibly inserted by CIL) 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_thd3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:822:3-822: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/mix008_tso.oepc.i:938:3-938: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/mix008_tso.oepc.i:938:3-938: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/mix008_tso.oepc.i:822:3-822:163)
[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/mix008_tso.oepc.i:822:3-822:163)
[Warning][Deadcode][CWE-571] condition '! z$w_buff1_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-570] condition '! z$r_buff0_thd4' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:884:3-884:228)
[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/mix008_tso.oepc.i:939:3-939:80)
[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 'z$r_buff0_thd4' (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-570] condition 'y$r_buff0_thd0' (possibly inserted by CIL) 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 '! y$w_buff1_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-570] condition 'y$w_buff1_used' (possibly inserted by CIL) 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' (possibly inserted by CIL) 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 '! y$r_buff0_thd3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:823:3-823:209)
[Warning][Deadcode][CWE-571] condition '! z$w_buff1_used' (possibly inserted by CIL) 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 '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 'y$r_buff0_thd3' (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-570] condition 'z$r_buff0_thd0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:941:3-941:104)
[Warning][Deadcode][CWE-571] condition '! z$w_buff1_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-570] condition 'z$w_buff1_used' (possibly inserted by CIL) 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_thd4' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:885:3-885: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:885:3-885:222)
[Warning][Deadcode][CWE-571] condition 'z$r_buff0_thd4' (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-570] condition 'z$r_buff0_thd0' (possibly inserted by CIL) 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 '! y$w_buff1_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$r_buff0_thd3' (possibly inserted by CIL) 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 '! y$r_buff0_thd3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:824:3-824:209)
[Warning][Deadcode][CWE-571] condition '! z$w_buff1_used' (possibly inserted by CIL) 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' (possibly inserted by CIL) 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 '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-570] condition 'z$w_buff1_used' (possibly inserted by CIL) 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 'y$r_buff0_thd3' (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_buff1_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)
[Warning][Deadcode][CWE-570] condition '! z$r_buff0_thd4' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:886:3-886:228)
[Warning][Deadcode][CWE-570] condition 'z$r_buff0_thd0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:944:3-944:80)
[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)
[Warning][Deadcode][CWE-571] condition 'z$r_buff0_thd4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:886:3-886:228)
[Warning][Deadcode][CWE-570] condition 'z$r_buff0_thd0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix008_tso.oepc.i:945:3-945:116)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 2
[Info][Race] Memory locations race summary:
  safe: 45
  vulnerable: 0
  unsafe: 0
  total memory locations: 45
