./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/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.127
[Info] vars: 480, evals: 1104

[Info] |called|=132

Memory statistics: total=659.23MB, max=15.81MB, minor=657.04MB, major=18.53MB, promoted=16.33MB
    minor collections=316  major collections=7 compactions=0


[Info] runtime: 00:00:20.152
[Info] vars: 582, evals: 1471

[Info] |called|=131

Memory statistics: total=957.40MB, max=15.81MB, minor=955.19MB, major=21.92MB, promoted=19.71MB
    minor collections=459  major collections=8 compactions=0


[Info] runtime: 00:00:30.193
[Info] vars: 606, evals: 1835

[Info] |called|=136

Memory statistics: total=1421.83MB, max=15.81MB, minor=1419.60MB, major=26.06MB, promoted=23.84MB
    minor collections=681  major collections=9 compactions=0


[Info] runtime: 00:00:40.212
[Info] vars: 617, evals: 2168

[Info] |called|=112

Memory statistics: total=1812.33MB, max=18.18MB, minor=1810.11MB, major=28.71MB, promoted=26.48MB
    minor collections=867  major collections=9 compactions=0


[Info] runtime: 00:00:50.228
[Info] vars: 653, evals: 2576

[Info] |called|=132

Memory statistics: total=2115.73MB, max=18.18MB, minor=2113.50MB, major=31.31MB, promoted=29.08MB
    minor collections=1012  major collections=10 compactions=0


[Info] runtime: 00:01:00.245
[Info] vars: 685, evals: 2985

[Info] |called|=129

Memory statistics: total=2418.42MB, max=18.18MB, minor=2416.18MB, major=33.78MB, promoted=31.55MB
    minor collections=1157  major collections=10 compactions=0


[Info] runtime: 00:01:10.252
[Info] vars: 713, evals: 3433

[Info] |called|=126

Memory statistics: total=2711.44MB, max=18.18MB, minor=2709.21MB, major=36.35MB, promoted=34.12MB
    minor collections=1297  major collections=11 compactions=0


[Info] runtime: 00:01:20.280
[Info] vars: 784, evals: 3928

[Info] |called|=126

Memory statistics: total=3080.30MB, max=18.18MB, minor=3078.06MB, major=40.97MB, promoted=38.72MB
    minor collections=1473  major collections=12 compactions=0


[Info] runtime: 00:01:30.301
[Info] vars: 792, evals: 4441

[Info] |called|=135

Memory statistics: total=3570.10MB, max=18.18MB, minor=3567.86MB, major=45.35MB, promoted=43.10MB
    minor collections=1707  major collections=13 compactions=0


[Info] runtime: 00:01:40.315
[Info] vars: 1016, evals: 5400

[Info] |called|=147

Memory statistics: total=4281.72MB, max=20.91MB, minor=4279.46MB, major=53.17MB, promoted=50.91MB
    minor collections=2047  major collections=14 compactions=0


[Info] runtime: 00:01:50.340
[Info] vars: 1059, evals: 5757

[Info] |called|=111

Memory statistics: total=4574.94MB, max=24.04MB, minor=4572.65MB, major=57.59MB, promoted=55.30MB
    minor collections=2187  major collections=15 compactions=0


[Info] runtime: 00:02:00.355
[Info] vars: 1200, evals: 6539

[Info] |called|=109

Memory statistics: total=5130.79MB, max=24.04MB, minor=5128.46MB, major=66.00MB, promoted=63.67MB
    minor collections=2453  major collections=16 compactions=0


[Info] runtime: 00:02:10.380
[Info] vars: 1247, evals: 7053

[Info] |called|=77

Memory statistics: total=5504.35MB, max=24.04MB, minor=5502.01MB, major=71.85MB, promoted=69.51MB
    minor collections=2632  major collections=17 compactions=0


[Info] runtime: 00:02:20.399
[Info] vars: 1269, evals: 7744

[Info] |called|=135

Memory statistics: total=5964.97MB, max=24.04MB, minor=5962.63MB, major=77.20MB, promoted=74.86MB
    minor collections=2852  major collections=18 compactions=0


[Info] runtime: 00:02:30.415
[Info] vars: 1291, evals: 8273

[Info] |called|=128

Memory statistics: total=6363.94MB, max=24.04MB, minor=6361.59MB, major=82.38MB, promoted=80.03MB
    minor collections=3042  major collections=18 compactions=0


[Info] runtime: 00:02:40.429
[Info] vars: 1312, evals: 8804

[Info] |called|=109

Memory statistics: total=6766.42MB, max=24.04MB, minor=6764.07MB, major=86.39MB, promoted=84.04MB
    minor collections=3234  major collections=19 compactions=0


[Info] runtime: 00:02:50.442
[Info] vars: 1339, evals: 9369

[Info] |called|=100

Memory statistics: total=7171.23MB, max=24.04MB, minor=7168.88MB, major=90.43MB, promoted=88.08MB
    minor collections=3428  major collections=20 compactions=0


[Info] runtime: 00:03:00.457
[Info] vars: 1379, evals: 9988

[Info] |called|=115

Memory statistics: total=7595.02MB, max=24.04MB, minor=7592.66MB, major=96.32MB, promoted=93.97MB
    minor collections=3630  major collections=20 compactions=0


[Info] runtime: 00:03:10.474
[Info] vars: 1510, evals: 10563

[Info] |called|=81

Memory statistics: total=8011.72MB, max=24.04MB, minor=8009.36MB, major=101.21MB, promoted=98.85MB
    minor collections=3829  major collections=21 compactions=0


[Info] runtime: 00:03:20.489
[Info] vars: 1533, evals: 11203

[Info] |called|=91

Memory statistics: total=8443.20MB, max=24.04MB, minor=8440.84MB, major=106.70MB, promoted=104.33MB
    minor collections=4036  major collections=22 compactions=0


[Info] runtime: 00:03:30.508
[Info] vars: 1567, evals: 11844

[Info] |called|=102

Memory statistics: total=8876.18MB, max=24.04MB, minor=8873.81MB, major=112.05MB, promoted=109.68MB
    minor collections=4242  major collections=23 compactions=0


[Info] runtime: 00:03:40.530
[Info] vars: 1569, evals: 12454

[Info] |called|=107

Memory statistics: total=9306.29MB, max=27.65MB, minor=9303.92MB, major=116.20MB, promoted=113.83MB
    minor collections=4448  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:03:50.532
[Info] vars: 1569, evals: 12771

[Info] |called|=0

Memory statistics: total=9741.59MB, max=27.65MB, minor=9739.19MB, major=121.00MB, promoted=118.60MB
    minor collections=4656  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)
[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] runtime: 00:04:00.587
[Info] vars: 1569, evals: 12771

[Info] |called|=0

Memory statistics: total=12607.72MB, max=27.65MB, minor=12605.06MB, major=135.56MB, promoted=132.90MB
    minor collections=6028  major collections=26 compactions=0


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

[Info] |called|=0

Memory statistics: total=18973.88MB, max=31.80MB, minor=18970.87MB, major=160.04MB, promoted=157.04MB
    minor collections=9077  major collections=29 compactions=0


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

[Info] |called|=0

Memory statistics: total=26613.26MB, max=31.80MB, minor=26609.84MB, major=189.25MB, promoted=185.83MB
    minor collections=12734  major collections=32 compactions=0


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

[Info] |called|=0

Memory statistics: total=35525.86MB, max=31.80MB, minor=35521.96MB, major=223.44MB, promoted=219.53MB
    minor collections=16998  major collections=36 compactions=0

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