./goblint --conf conf/svcomp-ghost.json --set ana.base.privatization mutex-meet --set 'ana.activated[+]' apron --set 'ana.autotune.activated[-]' octagon --set witness.yaml.entry-types '["invariant_set"]' --set witness.yaml.invariant-types '["location_invariant"]' --disable witness.invariant.loop-head --disable witness.invariant.other --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.156
[Info] vars: 503, evals: 956

[Info] |called|=129

Memory statistics: total=673.01MB, max=15.81MB, minor=670.82MB, major=19.71MB, promoted=17.52MB
    minor collections=323  major collections=7 compactions=0


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

[Info] |called|=128

Memory statistics: total=954.44MB, max=15.81MB, minor=952.23MB, major=22.87MB, promoted=20.66MB
    minor collections=458  major collections=8 compactions=0


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

[Info] |called|=114

Memory statistics: total=1383.41MB, max=15.81MB, minor=1381.18MB, major=26.78MB, promoted=24.56MB
    minor collections=663  major collections=9 compactions=0


[Info] runtime: 00:00:40.232
[Info] vars: 633, evals: 1954

[Info] |called|=139

Memory statistics: total=1756.45MB, max=18.18MB, minor=1754.22MB, major=29.39MB, promoted=27.16MB
    minor collections=840  major collections=9 compactions=0


[Info] runtime: 00:00:50.239
[Info] vars: 655, evals: 2283

[Info] |called|=130

Memory statistics: total=2102.02MB, max=18.18MB, minor=2099.79MB, major=31.88MB, promoted=29.65MB
    minor collections=1006  major collections=10 compactions=0


[Info] runtime: 00:01:00.248
[Info] vars: 686, evals: 2652

[Info] |called|=123

Memory statistics: total=2390.31MB, max=18.18MB, minor=2388.08MB, major=34.24MB, promoted=32.01MB
    minor collections=1143  major collections=10 compactions=0


[Info] runtime: 00:01:10.269
[Info] vars: 718, evals: 3059

[Info] |called|=129

Memory statistics: total=2658.69MB, max=18.18MB, minor=2656.46MB, major=36.43MB, promoted=34.20MB
    minor collections=1272  major collections=11 compactions=0


[Info] runtime: 00:01:20.286
[Info] vars: 753, evals: 3504

[Info] |called|=126

Memory statistics: total=2930.35MB, max=18.18MB, minor=2928.12MB, major=39.39MB, promoted=37.16MB
    minor collections=1401  major collections=11 compactions=0


[Info] runtime: 00:01:30.306
[Info] vars: 785, evals: 3931

[Info] |called|=86

Memory statistics: total=3239.28MB, max=18.18MB, minor=3237.04MB, major=43.28MB, promoted=41.04MB
    minor collections=1549  major collections=12 compactions=0


[Info] runtime: 00:01:40.327
[Info] vars: 1024, evals: 4485

[Info] |called|=118

Memory statistics: total=3584.86MB, max=18.18MB, minor=3582.61MB, major=47.42MB, promoted=45.17MB
    minor collections=1714  major collections=13 compactions=0


[Info] runtime: 00:01:50.349
[Info] vars: 1124, evals: 5049

[Info] |called|=146

Memory statistics: total=4099.85MB, max=20.91MB, minor=4097.57MB, major=52.90MB, promoted=50.62MB
    minor collections=1960  major collections=14 compactions=0


[Info] runtime: 00:02:00.377
[Info] vars: 1220, evals: 5563

[Info] |called|=126

Memory statistics: total=4644.07MB, max=20.91MB, minor=4641.77MB, major=58.30MB, promoted=56.00MB
    minor collections=2220  major collections=15 compactions=0


[Info] runtime: 00:02:10.407
[Info] vars: 1244, evals: 6066

[Info] |called|=125

Memory statistics: total=5123.54MB, max=24.04MB, minor=5121.24MB, major=63.73MB, promoted=61.42MB
    minor collections=2449  major collections=15 compactions=0


[Info] runtime: 00:02:20.426
[Info] vars: 1279, evals: 6456

[Info] |called|=83

Memory statistics: total=5422.42MB, max=24.04MB, minor=5420.09MB, major=68.54MB, promoted=66.20MB
    minor collections=2592  major collections=16 compactions=0


[Info] runtime: 00:02:30.436
[Info] vars: 1301, evals: 6961

[Info] |called|=100

Memory statistics: total=5818.31MB, max=24.04MB, minor=5815.97MB, major=73.22MB, promoted=70.88MB
    minor collections=2781  major collections=17 compactions=0


[Info] runtime: 00:02:40.457
[Info] vars: 1322, evals: 7446

[Info] |called|=106

Memory statistics: total=6217.60MB, max=24.04MB, minor=6215.25MB, major=77.86MB, promoted=75.52MB
    minor collections=2972  major collections=17 compactions=0


[Info] runtime: 00:02:50.466
[Info] vars: 1352, evals: 7938

[Info] |called|=120

Memory statistics: total=6613.51MB, max=24.04MB, minor=6611.16MB, major=83.02MB, promoted=80.67MB
    minor collections=3161  major collections=18 compactions=0


[Info] runtime: 00:03:00.478
[Info] vars: 1373, evals: 8438

[Info] |called|=129

Memory statistics: total=7013.04MB, max=24.04MB, minor=7010.69MB, major=86.83MB, promoted=84.48MB
    minor collections=3352  major collections=19 compactions=0


[Info] runtime: 00:03:10.493
[Info] vars: 1400, evals: 8952

[Info] |called|=135

Memory statistics: total=7422.91MB, max=27.65MB, minor=7420.56MB, major=90.74MB, promoted=88.39MB
    minor collections=3547  major collections=19 compactions=0


[Info] runtime: 00:03:20.506
[Info] vars: 1400, evals: 9313

[Info] |called|=81

Memory statistics: total=7763.82MB, max=27.65MB, minor=7761.47MB, major=93.48MB, promoted=91.12MB
    minor collections=3711  major collections=20 compactions=0


[Info] runtime: 00:03:30.546
[Info] vars: 1448, evals: 9842

[Info] |called|=124

Memory statistics: total=8135.06MB, max=27.65MB, minor=8132.71MB, major=98.91MB, promoted=96.55MB
    minor collections=3888  major collections=20 compactions=0


[Info] runtime: 00:03:40.576
[Info] vars: 1579, evals: 10335

[Info] |called|=108

Memory statistics: total=8535.23MB, max=27.65MB, minor=8532.86MB, major=103.77MB, promoted=101.40MB
    minor collections=4079  major collections=21 compactions=0


[Info] runtime: 00:03:50.592
[Info] vars: 1602, evals: 10929

[Info] |called|=136

Memory statistics: total=8954.36MB, max=27.65MB, minor=8952.00MB, major=108.08MB, promoted=105.72MB
    minor collections=4279  major collections=22 compactions=0


[Info] runtime: 00:04:00.605
[Info] vars: 1623, evals: 11307

[Info] |called|=66

Memory statistics: total=9310.53MB, max=27.65MB, minor=9308.16MB, major=113.35MB, promoted=110.98MB
    minor collections=4449  major collections=22 compactions=0


[Info] runtime: 00:04:10.620
[Info] vars: 1644, evals: 11811

[Info] |called|=79

Memory statistics: total=9651.36MB, max=27.65MB, minor=9648.98MB, major=117.05MB, promoted=114.68MB
    minor collections=4612  major collections=23 compactions=0


[Info] runtime: 00:04:20.639
[Info] vars: 1646, evals: 12385

[Info] |called|=129

Memory statistics: total=10075.80MB, max=27.65MB, minor=10073.42MB, major=121.27MB, promoted=118.89MB
    minor collections=4814  major collections=23 compactions=0


[Info] runtime: 00:04:30.646
[Info] vars: 1646, evals: 12789

[Info] |called|=9

Memory statistics: total=10459.45MB, max=27.65MB, minor=10457.07MB, major=124.62MB, promoted=122.24MB
    minor collections=4998  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)
[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)

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

[Info] |called|=0

Memory statistics: total=10831.48MB, max=27.65MB, minor=10829.07MB, major=129.31MB, promoted=126.90MB
    minor collections=5175  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: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] runtime: 00:04:50.679
[Info] vars: 1646, evals: 12790

[Info] |called|=0

Memory statistics: total=15258.63MB, max=31.80MB, minor=15255.81MB, major=149.07MB, promoted=146.26MB
    minor collections=7296  major collections=27 compactions=0


[Info] runtime: 00:05:00.686
[Info] vars: 1646, evals: 12790

[Info] |called|=0

Memory statistics: total=21899.42MB, max=36.57MB, minor=21896.27MB, major=174.34MB, promoted=171.20MB
    minor collections=10476  major collections=29 compactions=0


[Info] runtime: 00:05:10.703
[Info] vars: 1646, evals: 12790

[Info] |called|=0

Memory statistics: total=29139.16MB, max=36.57MB, minor=29135.62MB, major=202.08MB, promoted=198.54MB
    minor collections=13942  major collections=32 compactions=0


[Info] runtime: 00:05:20.717
[Info] vars: 1646, evals: 12790

[Info] |called|=0

Memory statistics: total=35172.29MB, max=36.57MB, minor=35168.41MB, major=225.20MB, promoted=221.33MB
    minor collections=16834  major collections=35 compactions=0

[Info][Witness] witness generation summary:
  total generation entries: 1
[Info][Race] Memory locations race summary:
  safe: 45
  vulnerable: 0
  unsafe: 0
  total memory locations: 45
