./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/mix006_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.161
[Info] vars: 493, evals: 1211

[Info] |called|=126

Memory statistics: total=725.17MB, max=15.81MB, minor=723.00MB, major=18.77MB, promoted=16.60MB
    minor collections=348  major collections=7 compactions=0


[Info] runtime: 00:00:20.185
[Info] vars: 586, evals: 1693

[Info] |called|=142

Memory statistics: total=1153.96MB, max=15.81MB, minor=1151.76MB, major=23.75MB, promoted=21.56MB
    minor collections=553  major collections=8 compactions=0


[Info] runtime: 00:00:30.206
[Info] vars: 598, evals: 2113

[Info] |called|=138

Memory statistics: total=1730.47MB, max=15.81MB, minor=1728.27MB, major=27.41MB, promoted=25.22MB
    minor collections=828  major collections=9 compactions=0


[Info] runtime: 00:00:40.225
[Info] vars: 635, evals: 2582

[Info] |called|=132

Memory statistics: total=2143.53MB, max=18.18MB, minor=2141.32MB, major=30.65MB, promoted=28.45MB
    minor collections=1026  major collections=10 compactions=0


[Info] runtime: 00:00:50.245
[Info] vars: 683, evals: 3140

[Info] |called|=139

Memory statistics: total=2504.86MB, max=18.18MB, minor=2502.65MB, major=33.73MB, promoted=31.52MB
    minor collections=1198  major collections=10 compactions=0


[Info] runtime: 00:01:00.260
[Info] vars: 718, evals: 3675

[Info] |called|=125

Memory statistics: total=2857.33MB, max=18.18MB, minor=2855.12MB, major=37.20MB, promoted=34.99MB
    minor collections=1366  major collections=11 compactions=0


[Info] runtime: 00:01:10.297
[Info] vars: 768, evals: 4245

[Info] |called|=105

Memory statistics: total=3410.87MB, max=18.18MB, minor=3408.65MB, major=42.52MB, promoted=40.31MB
    minor collections=1631  major collections=12 compactions=0


[Info] runtime: 00:01:20.309
[Info] vars: 1048, evals: 4975

[Info] |called|=113

Memory statistics: total=3929.23MB, max=18.18MB, minor=3926.98MB, major=48.10MB, promoted=45.85MB
    minor collections=1879  major collections=13 compactions=0


[Info] runtime: 00:01:30.333
[Info] vars: 1149, evals: 5740

[Info] |called|=127

Memory statistics: total=4685.23MB, max=20.91MB, minor=4682.95MB, major=55.71MB, promoted=53.43MB
    minor collections=2240  major collections=14 compactions=0


[Info] runtime: 00:01:40.354
[Info] vars: 1227, evals: 6433

[Info] |called|=110

Memory statistics: total=5313.21MB, max=24.04MB, minor=5310.93MB, major=62.85MB, promoted=60.56MB
    minor collections=2540  major collections=15 compactions=0


[Info] runtime: 00:01:50.371
[Info] vars: 1284, evals: 7141

[Info] |called|=148

Memory statistics: total=5788.77MB, max=24.04MB, minor=5786.45MB, major=70.01MB, promoted=67.69MB
    minor collections=2767  major collections=16 compactions=0


[Info] runtime: 00:02:00.384
[Info] vars: 1305, evals: 7707

[Info] |called|=123

Memory statistics: total=6262.08MB, max=24.04MB, minor=6259.76MB, major=74.80MB, promoted=72.48MB
    minor collections=2993  major collections=17 compactions=0


[Info] runtime: 00:02:10.396
[Info] vars: 1335, evals: 8305

[Info] |called|=102

Memory statistics: total=6726.32MB, max=24.04MB, minor=6723.99MB, major=80.64MB, promoted=78.31MB
    minor collections=3215  major collections=18 compactions=0


[Info] runtime: 00:02:20.416
[Info] vars: 1356, evals: 8952

[Info] |called|=126

Memory statistics: total=7211.47MB, max=24.04MB, minor=7209.14MB, major=85.08MB, promoted=82.75MB
    minor collections=3446  major collections=18 compactions=0


[Info] runtime: 00:02:30.429
[Info] vars: 1383, evals: 9576

[Info] |called|=95

Memory statistics: total=7736.14MB, max=24.04MB, minor=7733.81MB, major=89.50MB, promoted=87.17MB
    minor collections=3697  major collections=19 compactions=0


[Info] runtime: 00:02:40.457
[Info] vars: 1458, evals: 10217

[Info] |called|=28

Memory statistics: total=8253.16MB, max=27.65MB, minor=8250.82MB, major=96.65MB, promoted=94.31MB
    minor collections=3944  major collections=20 compactions=0


[Info] runtime: 00:02:50.472
[Info] vars: 1561, evals: 10886

[Info] |called|=23

Memory statistics: total=8744.72MB, max=27.65MB, minor=8742.38MB, major=101.42MB, promoted=99.07MB
    minor collections=4179  major collections=21 compactions=0


[Info] runtime: 00:03:00.496
[Info] vars: 1613, evals: 11595

[Info] |called|=21

Memory statistics: total=9245.02MB, max=27.65MB, minor=9242.67MB, major=108.51MB, promoted=106.16MB
    minor collections=4417  major collections=21 compactions=0


[Info] runtime: 00:03:10.522
[Info] vars: 1626, evals: 12275

[Info] |called|=23

Memory statistics: total=9745.20MB, max=27.65MB, minor=9742.84MB, major=113.19MB, promoted=110.84MB
    minor collections=4656  major collections=22 compactions=0


[Info] runtime: 00:03:20.537
[Info] vars: 1628, evals: 12941

[Info] |called|=23

Memory statistics: total=10240.05MB, max=27.65MB, minor=10237.69MB, major=117.45MB, promoted=115.09MB
    minor collections=4893  major collections=23 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:776:3-776:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:834:3-834:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:884:3-884:42)

[Info] runtime: 00:03:30.548
[Info] vars: 1628, evals: 12988

[Info] |called|=0

Memory statistics: total=10742.19MB, max=27.65MB, minor=10739.78MB, major=123.73MB, promoted=121.33MB
    minor collections=5132  major collections=23 compactions=0

[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_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/mix006_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/mix006_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/mix006_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/mix006_tso.oepc.i:105:1-109:1)
[Warning][Deadcode] Function 'fence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:888:1-890:1)
[Warning][Deadcode] Function 'isync' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:891:1-893:1)
[Warning][Deadcode] Function 'lwfence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:894:1-896:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 166
  dead: 8 (8 in uncalled functions)
  total lines: 174
[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/mix006_tso.oepc.i:863:3-863:222)
[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/mix006_tso.oepc.i:926:3-926:163)
[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/mix006_tso.oepc.i:926:3-926:163)
[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/mix006_tso.oepc.i:863:3-863: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/mix006_tso.oepc.i:863:3-863: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/mix006_tso.oepc.i:803:3-803: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/mix006_tso.oepc.i:803:3-803: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/mix006_tso.oepc.i:803:3-803: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/mix006_tso.oepc.i:803:3-803:222)
[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/mix006_tso.oepc.i:927:3-927: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/mix006_tso.oepc.i:827:3-827: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/mix006_tso.oepc.i:927:3-927:209)
[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/mix006_tso.oepc.i:872:3-872: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/mix006_tso.oepc.i:872:3-872: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/mix006_tso.oepc.i:804:3-804: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/mix006_tso.oepc.i:804:3-804: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/mix006_tso.oepc.i:804:3-804: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/mix006_tso.oepc.i:829:3-829: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/mix006_tso.oepc.i:804:3-804:228)
[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/mix006_tso.oepc.i:873:3-873: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/mix006_tso.oepc.i:928:3-928: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/mix006_tso.oepc.i:928:3-928:209)
[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/mix006_tso.oepc.i:874:3-874: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/mix006_tso.oepc.i:874:3-874:116)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006_tso.oepc.i:17:73-17:74)
[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/mix006_tso.oepc.i:805:3-805: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/mix006_tso.oepc.i:831:3-831: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/mix006_tso.oepc.i:875:3-875:80)
[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/mix006_tso.oepc.i:805:3-805: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/mix006_tso.oepc.i:805:3-805: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/mix006_tso.oepc.i:805:3-805:222)
[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/mix006_tso.oepc.i:876:3-876: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/mix006_tso.oepc.i:876:3-876: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/mix006_tso.oepc.i:929:3-929: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/mix006_tso.oepc.i:929:3-929: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/mix006_tso.oepc.i:845:3-845:57)
[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/mix006_tso.oepc.i:769:3-769: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/mix006_tso.oepc.i:877:3-877: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/mix006_tso.oepc.i:769:3-769: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/mix006_tso.oepc.i:815:3-815: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/mix006_tso.oepc.i:815:3-815: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/mix006_tso.oepc.i:770:3-770: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/mix006_tso.oepc.i:930:3-930: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/mix006_tso.oepc.i:930:3-930: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/mix006_tso.oepc.i:879:3-879: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/mix006_tso.oepc.i:857:3-857: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/mix006_tso.oepc.i:771:3-771: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/mix006_tso.oepc.i:857:3-857:163)
[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/mix006_tso.oepc.i:771:3-771: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/mix006_tso.oepc.i:857:3-857: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/mix006_tso.oepc.i:857:3-857: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/mix006_tso.oepc.i:772:3-772: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/mix006_tso.oepc.i:816:3-816: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/mix006_tso.oepc.i:816:3-816: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/mix006_tso.oepc.i:881:3-881: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/mix006_tso.oepc.i:773:3-773: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/mix006_tso.oepc.i:931:3-931: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/mix006_tso.oepc.i:931:3-931: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/mix006_tso.oepc.i:773:3-773: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/mix006_tso.oepc.i:858:3-858:209)
[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/mix006_tso.oepc.i:858:3-858: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/mix006_tso.oepc.i:858:3-858: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/mix006_tso.oepc.i:858:3-858: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/mix006_tso.oepc.i:817:3-817: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/mix006_tso.oepc.i:817:3-817: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/mix006_tso.oepc.i:787:3-787: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/mix006_tso.oepc.i:932:3-932: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/mix006_tso.oepc.i:910:3-910: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/mix006_tso.oepc.i:932:3-932: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/mix006_tso.oepc.i:910:3-910: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/mix006_tso.oepc.i:859:3-859:209)
[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/mix006_tso.oepc.i:859:3-859: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/mix006_tso.oepc.i:859:3-859: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/mix006_tso.oepc.i:859:3-859: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/mix006_tso.oepc.i:911:3-911: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/mix006_tso.oepc.i:799:3-799: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/mix006_tso.oepc.i:818:3-818:228)
[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/mix006_tso.oepc.i:912:3-912: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/mix006_tso.oepc.i:818:3-818: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/mix006_tso.oepc.i:799:3-799:163)
[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/mix006_tso.oepc.i:912:3-912: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/mix006_tso.oepc.i:799:3-799:163)
[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/mix006_tso.oepc.i:799:3-799: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/mix006_tso.oepc.i:860:3-860:228)
[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/mix006_tso.oepc.i:913:3-913:80)
[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/mix006_tso.oepc.i:860:3-860: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/mix006_tso.oepc.i:860:3-860: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/mix006_tso.oepc.i:860:3-860:228)
[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/mix006_tso.oepc.i:914:3-914: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/mix006_tso.oepc.i:914:3-914: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/mix006_tso.oepc.i:800:3-800: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/mix006_tso.oepc.i:819:3-819: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/mix006_tso.oepc.i:800:3-800: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/mix006_tso.oepc.i:819:3-819: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/mix006_tso.oepc.i:915:3-915: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/mix006_tso.oepc.i:800:3-800: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/mix006_tso.oepc.i:800:3-800: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/mix006_tso.oepc.i:915:3-915: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/mix006_tso.oepc.i:861:3-861: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/mix006_tso.oepc.i:861:3-861: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/mix006_tso.oepc.i:861:3-861: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/mix006_tso.oepc.i:861:3-861: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/mix006_tso.oepc.i:916:3-916: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/mix006_tso.oepc.i:801:3-801: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/mix006_tso.oepc.i:820:3-820: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/mix006_tso.oepc.i:801:3-801: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/mix006_tso.oepc.i:917:3-917: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/mix006_tso.oepc.i:820:3-820: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/mix006_tso.oepc.i:917:3-917: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/mix006_tso.oepc.i:801:3-801: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/mix006_tso.oepc.i:801:3-801: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/mix006_tso.oepc.i:862:3-862: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/mix006_tso.oepc.i:918:3-918:80)
[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/mix006_tso.oepc.i:862:3-862: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/mix006_tso.oepc.i:862:3-862: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/mix006_tso.oepc.i:862:3-862: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/mix006_tso.oepc.i:919:3-919: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/mix006_tso.oepc.i:919:3-919: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/mix006_tso.oepc.i:802:3-802:228)
[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/mix006_tso.oepc.i:821:3-821: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/mix006_tso.oepc.i:802:3-802: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/mix006_tso.oepc.i:821:3-821: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/mix006_tso.oepc.i:802:3-802: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/mix006_tso.oepc.i:802:3-802: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/mix006_tso.oepc.i:863:3-863:222)
SV-COMP result: unknown

[Info] runtime: 00:03:40.585
[Info] vars: 1628, evals: 12988

[Info] |called|=0

Memory statistics: total=17364.69MB, max=31.80MB, minor=17361.81MB, major=150.46MB, promoted=147.58MB
    minor collections=8303  major collections=26 compactions=0


[Info] runtime: 00:03:50.596
[Info] vars: 1628, evals: 12988

[Info] |called|=0

Memory statistics: total=25783.90MB, max=36.57MB, minor=25780.54MB, major=182.84MB, promoted=179.48MB
    minor collections=12330  major collections=30 compactions=0

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