./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/rfi002_tso.i


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


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

[Info] runtime: 00:00:10.128
[Info] vars: 417, evals: 1953

[Info] |called|=100

Memory statistics: total=796.79MB, max=15.81MB, minor=794.60MB, major=19.48MB, promoted=17.29MB
    minor collections=382  major collections=7 compactions=0


[Info] runtime: 00:00:20.158
[Info] vars: 670, evals: 3252

[Info] |called|=170

Memory statistics: total=1381.82MB, max=15.81MB, minor=1379.59MB, major=27.20MB, promoted=24.97MB
    minor collections=662  major collections=9 compactions=0


[Info] runtime: 00:00:30.174
[Info] vars: 813, evals: 3683

[Info] |called|=137

Memory statistics: total=1730.11MB, max=15.81MB, minor=1727.87MB, major=30.70MB, promoted=28.46MB
    minor collections=828  major collections=10 compactions=0


[Info] runtime: 00:00:40.199
[Info] vars: 1005, evals: 4210

[Info] |called|=144

Memory statistics: total=2226.63MB, max=18.18MB, minor=2224.37MB, major=36.43MB, promoted=34.18MB
    minor collections=1066  major collections=11 compactions=0


[Info] runtime: 00:00:50.215
[Info] vars: 1089, evals: 4700

[Info] |called|=147

Memory statistics: total=2669.81MB, max=18.18MB, minor=2667.54MB, major=40.24MB, promoted=37.97MB
    minor collections=1278  major collections=12 compactions=0


[Info] runtime: 00:01:00.239
[Info] vars: 1149, evals: 5178

[Info] |called|=141

Memory statistics: total=3158.61MB, max=20.91MB, minor=3156.31MB, major=46.05MB, promoted=43.75MB
    minor collections=1511  major collections=13 compactions=0


[Info] runtime: 00:01:10.268
[Info] vars: 1233, evals: 5610

[Info] |called|=102

Memory statistics: total=3806.98MB, max=20.91MB, minor=3804.64MB, major=52.54MB, promoted=50.20MB
    minor collections=1821  major collections=14 compactions=0


[Info] runtime: 00:01:20.282
[Info] vars: 1265, evals: 6249

[Info] |called|=85

Memory statistics: total=4509.38MB, max=24.04MB, minor=4507.04MB, major=58.59MB, promoted=56.25MB
    minor collections=2156  major collections=14 compactions=0


[Info] runtime: 00:01:30.304
[Info] vars: 1328, evals: 6784

[Info] |called|=116

Memory statistics: total=5039.97MB, max=27.65MB, minor=5037.61MB, major=64.91MB, promoted=62.55MB
    minor collections=2409  major collections=15 compactions=0


[Info] runtime: 00:01:40.318
[Info] vars: 1333, evals: 7460

[Info] |called|=116

Memory statistics: total=5671.41MB, max=27.65MB, minor=5669.04MB, major=70.97MB, promoted=68.61MB
    minor collections=2711  major collections=16 compactions=0


[Info] runtime: 00:01:50.333
[Info] vars: 1376, evals: 8088

[Info] |called|=120

Memory statistics: total=6132.10MB, max=27.65MB, minor=6129.72MB, major=77.51MB, promoted=75.14MB
    minor collections=2931  major collections=17 compactions=0


[Info] runtime: 00:02:00.347
[Info] vars: 1397, evals: 8807

[Info] |called|=156

Memory statistics: total=6612.12MB, max=27.65MB, minor=6609.74MB, major=81.95MB, promoted=79.57MB
    minor collections=3160  major collections=18 compactions=0


[Info] runtime: 00:02:10.361
[Info] vars: 1424, evals: 9391

[Info] |called|=141

Memory statistics: total=7073.73MB, max=27.65MB, minor=7071.36MB, major=85.97MB, promoted=83.59MB
    minor collections=3380  major collections=18 compactions=0


[Info] runtime: 00:02:20.379
[Info] vars: 1464, evals: 10002

[Info] |called|=124

Memory statistics: total=7536.56MB, max=27.65MB, minor=7534.18MB, major=91.42MB, promoted=89.03MB
    minor collections=3602  major collections=19 compactions=0


[Info] runtime: 00:02:30.387
[Info] vars: 1589, evals: 10668

[Info] |called|=122

Memory statistics: total=8008.07MB, max=27.65MB, minor=8005.68MB, major=96.92MB, promoted=94.53MB
    minor collections=3827  major collections=20 compactions=0


[Info] runtime: 00:02:40.398
[Info] vars: 1625, evals: 11356

[Info] |called|=115

Memory statistics: total=8491.97MB, max=27.65MB, minor=8489.57MB, major=102.69MB, promoted=100.29MB
    minor collections=4058  major collections=20 compactions=0


[Info] runtime: 00:02:50.427
[Info] vars: 1642, evals: 12040

[Info] |called|=115

Memory statistics: total=8976.78MB, max=27.65MB, minor=8974.38MB, major=108.17MB, promoted=105.77MB
    minor collections=4289  major collections=21 compactions=0


[Info] runtime: 00:03:00.438
[Info] vars: 1644, evals: 12711

[Info] |called|=108

Memory statistics: total=9461.71MB, max=27.65MB, minor=9459.30MB, major=112.53MB, promoted=110.13MB
    minor collections=4521  major collections=22 compactions=0

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

[Info] runtime: 00:03:10.448
[Info] vars: 1644, evals: 12846

[Info] |called|=0

Memory statistics: total=9948.44MB, max=27.65MB, minor=9946.00MB, major=118.38MB, promoted=115.95MB
    minor collections=4754  major collections=23 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:861:3-861:42)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:86:1-90:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:91:1-95:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:96:1-100:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:101:1-105:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:106:1-110:1)
[Warning][Deadcode] Function 'fence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:865:1-867:1)
[Warning][Deadcode] Function 'isync' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:868:1-870:1)
[Warning][Deadcode] Function 'lwfence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:871:1-873:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 152
  dead: 8 (8 in uncalled functions)
  total lines: 160
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:774:3-774: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/rfi002_tso.i:825:3-825: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/rfi002_tso.i:774:3-774:228)
[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/rfi002_tso.i:902:3-902: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/rfi002_tso.i:825:3-825: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/rfi002_tso.i:902:3-902: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/rfi002_tso.i:825:3-825:222)
[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/rfi002_tso.i:825:3-825: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/rfi002_tso.i:849:3-849:104)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:775:3-775: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/rfi002_tso.i:826:3-826: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/rfi002_tso.i:775:3-775: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/rfi002_tso.i:903:3-903: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/rfi002_tso.i:826:3-826: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/rfi002_tso.i:903:3-903: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/rfi002_tso.i:826:3-826: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/rfi002_tso.i:826:3-826: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/rfi002_tso.i:851:3-851: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/rfi002_tso.i:827:3-827:222)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:18:73-18: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/rfi002_tso.i:904:3-904: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/rfi002_tso.i:853:3-853:116)
[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/rfi002_tso.i:827:3-827: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/rfi002_tso.i:904:3-904:228)
[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/rfi002_tso.i:781:3-781:104)
[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/rfi002_tso.i:827:3-827:222)
[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/rfi002_tso.i:827:3-827: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/rfi002_tso.i:781:3-781: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/rfi002_tso.i:854:3-854: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/rfi002_tso.i:782:3-782: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/rfi002_tso.i:758:3-758: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/rfi002_tso.i:783:3-783: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/rfi002_tso.i:905:3-905: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/rfi002_tso.i:758:3-758: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/rfi002_tso.i:905:3-905: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/rfi002_tso.i:783:3-783: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/rfi002_tso.i:856:3-856: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/rfi002_tso.i:837:3-837: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/rfi002_tso.i:784:3-784: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/rfi002_tso.i:759:3-759: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/rfi002_tso.i:837:3-837: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/rfi002_tso.i:785:3-785: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/rfi002_tso.i:760:3-760: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/rfi002_tso.i:837:3-837: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/rfi002_tso.i:837:3-837: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/rfi002_tso.i:785:3-785: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/rfi002_tso.i:760:3-760: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/rfi002_tso.i:906:3-906: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/rfi002_tso.i:858:3-858: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/rfi002_tso.i:906:3-906:228)
[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/rfi002_tso.i:761:3-761: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/rfi002_tso.i:838:3-838:209)
[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/rfi002_tso.i:762:3-762: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/rfi002_tso.i:838:3-838: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/rfi002_tso.i:762:3-762: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/rfi002_tso.i:799:3-799:57)
[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/rfi002_tso.i:838:3-838: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/rfi002_tso.i:838:3-838: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/rfi002_tso.i:907:3-907: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/rfi002_tso.i:885:3-885: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/rfi002_tso.i:907:3-907: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/rfi002_tso.i:885:3-885:104)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:769:3-769: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/rfi002_tso.i:769:3-769: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/rfi002_tso.i:839:3-839: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/rfi002_tso.i:810:3-810:57)
[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/rfi002_tso.i:839:3-839: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/rfi002_tso.i:886:3-886:80)
[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/rfi002_tso.i:839:3-839: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/rfi002_tso.i:839:3-839: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/rfi002_tso.i:887:3-887: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/rfi002_tso.i:887:3-887:116)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:770:3-770: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/rfi002_tso.i:770:3-770: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/rfi002_tso.i:821:3-821: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/rfi002_tso.i:888:3-888: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/rfi002_tso.i:840:3-840:228)
[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/rfi002_tso.i:821:3-821:163)
[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/rfi002_tso.i:840:3-840: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/rfi002_tso.i:821:3-821: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/rfi002_tso.i:889:3-889: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/rfi002_tso.i:821:3-821:163)
[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/rfi002_tso.i:840:3-840: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/rfi002_tso.i:889:3-889: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/rfi002_tso.i:840:3-840: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/rfi002_tso.i:890:3-890:104)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:771:3-771: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/rfi002_tso.i:822:3-822: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/rfi002_tso.i:771:3-771: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/rfi002_tso.i:890:3-890:104)
[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/rfi002_tso.i:822:3-822: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/rfi002_tso.i:841:3-841: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/rfi002_tso.i:841:3-841: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/rfi002_tso.i:822:3-822: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/rfi002_tso.i:822:3-822: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/rfi002_tso.i:891:3-891:80)
[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/rfi002_tso.i:841:3-841: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/rfi002_tso.i:841:3-841: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/rfi002_tso.i:892:3-892: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/rfi002_tso.i:892:3-892:116)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:772:3-772: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/rfi002_tso.i:823:3-823: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/rfi002_tso.i:772:3-772:228)
[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/rfi002_tso.i:823:3-823: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/rfi002_tso.i:893:3-893: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/rfi002_tso.i:842:3-842: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/rfi002_tso.i:842:3-842: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/rfi002_tso.i:823:3-823: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/rfi002_tso.i:823:3-823: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/rfi002_tso.i:894:3-894: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/rfi002_tso.i:842:3-842: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/rfi002_tso.i:894:3-894: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/rfi002_tso.i:842:3-842:228)
[Warning][Deadcode][CWE-571] condition '! x$r_buff0_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:773:3-773: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/rfi002_tso.i:824:3-824: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/rfi002_tso.i:773:3-773: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/rfi002_tso.i:824:3-824:228)
[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/rfi002_tso.i:901:3-901: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/rfi002_tso.i:843:3-843: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/rfi002_tso.i:901:3-901:163)
[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/rfi002_tso.i:843:3-843: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/rfi002_tso.i:824:3-824: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/rfi002_tso.i:824:3-824: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/rfi002_tso.i:843:3-843: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/rfi002_tso.i:843:3-843:222)
SV-COMP result: unknown

[Info] runtime: 00:03:20.466
[Info] vars: 1644, evals: 12846

[Info] |called|=0

Memory statistics: total=15337.05MB, max=31.80MB, minor=15334.19MB, major=141.55MB, promoted=138.69MB
    minor collections=7329  major collections=25 compactions=0

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