./goblint --conf conf/svcomp-ghost.json --set ana.base.privatization mutex-meet --set 'ana.activated[+]' apron --set 'ana.autotune.activated[-]' octagon --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/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.119
[Info] vars: 417, evals: 1974

[Info] |called|=95

Memory statistics: total=803.23MB, max=15.81MB, minor=801.03MB, major=19.41MB, promoted=17.21MB
    minor collections=385  major collections=7 compactions=0


[Info] runtime: 00:00:20.151
[Info] vars: 670, evals: 3253

[Info] |called|=160

Memory statistics: total=1387.91MB, max=15.81MB, minor=1385.68MB, major=27.00MB, promoted=24.77MB
    minor collections=665  major collections=9 compactions=0


[Info] runtime: 00:00:30.165
[Info] vars: 815, evals: 3736

[Info] |called|=178

Memory statistics: total=1737.35MB, max=15.81MB, minor=1735.11MB, major=30.68MB, promoted=28.44MB
    minor collections=832  major collections=10 compactions=0


[Info] runtime: 00:00:40.202
[Info] vars: 1005, evals: 4225

[Info] |called|=142

Memory statistics: total=2260.15MB, max=18.18MB, minor=2257.90MB, major=36.38MB, promoted=34.12MB
    minor collections=1082  major collections=11 compactions=0


[Info] runtime: 00:00:50.225
[Info] vars: 1089, evals: 4716

[Info] |called|=147

Memory statistics: total=2670.34MB, max=20.91MB, minor=2668.07MB, major=40.37MB, promoted=38.10MB
    minor collections=1278  major collections=12 compactions=0


[Info] runtime: 00:01:00.246
[Info] vars: 1149, evals: 5197

[Info] |called|=137

Memory statistics: total=3162.63MB, max=20.91MB, minor=3160.33MB, major=46.23MB, promoted=43.92MB
    minor collections=1512  major collections=12 compactions=0


[Info] runtime: 00:01:10.280
[Info] vars: 1233, evals: 5623

[Info] |called|=87

Memory statistics: total=3834.10MB, max=20.91MB, minor=3831.76MB, major=52.98MB, promoted=50.64MB
    minor collections=1834  major collections=14 compactions=0


[Info] runtime: 00:01:20.296
[Info] vars: 1281, evals: 6378

[Info] |called|=163

Memory statistics: total=4527.84MB, max=24.04MB, minor=4525.50MB, major=59.09MB, promoted=56.74MB
    minor collections=2164  major collections=14 compactions=0


[Info] runtime: 00:01:30.316
[Info] vars: 1328, evals: 6802

[Info] |called|=117

Memory statistics: total=5058.15MB, max=27.65MB, minor=5055.79MB, major=65.10MB, promoted=62.74MB
    minor collections=2418  major collections=15 compactions=0


[Info] runtime: 00:01:40.331
[Info] vars: 1333, evals: 7478

[Info] |called|=105

Memory statistics: total=5743.92MB, max=27.65MB, minor=5741.56MB, major=71.04MB, promoted=68.67MB
    minor collections=2745  major collections=16 compactions=0


[Info] runtime: 00:01:50.342
[Info] vars: 1376, evals: 8154

[Info] |called|=102

Memory statistics: total=6222.72MB, max=27.65MB, minor=6220.35MB, major=77.55MB, promoted=75.18MB
    minor collections=2974  major collections=17 compactions=0


[Info] runtime: 00:02:00.367
[Info] vars: 1397, evals: 8831

[Info] |called|=144

Memory statistics: total=6689.87MB, max=27.65MB, minor=6687.49MB, major=81.95MB, promoted=79.57MB
    minor collections=3197  major collections=18 compactions=0


[Info] runtime: 00:02:10.376
[Info] vars: 1424, evals: 9417

[Info] |called|=135

Memory statistics: total=7149.36MB, max=27.65MB, minor=7146.99MB, major=85.83MB, promoted=83.46MB
    minor collections=3417  major collections=18 compactions=0


[Info] runtime: 00:02:20.397
[Info] vars: 1464, evals: 10024

[Info] |called|=118

Memory statistics: total=7604.45MB, max=27.65MB, minor=7602.06MB, major=91.36MB, promoted=88.97MB
    minor collections=3634  major collections=19 compactions=0


[Info] runtime: 00:02:30.411
[Info] vars: 1589, evals: 10693

[Info] |called|=114

Memory statistics: total=8088.05MB, max=27.65MB, minor=8085.66MB, major=96.91MB, promoted=94.52MB
    minor collections=3865  major collections=20 compactions=0


[Info] runtime: 00:02:40.433
[Info] vars: 1625, evals: 11387

[Info] |called|=114

Memory statistics: total=8566.98MB, max=27.65MB, minor=8564.59MB, major=102.71MB, promoted=100.31MB
    minor collections=4094  major collections=20 compactions=0


[Info] runtime: 00:02:50.460
[Info] vars: 1642, evals: 12066

[Info] |called|=97

Memory statistics: total=9058.32MB, max=27.65MB, minor=9055.92MB, major=107.98MB, promoted=105.57MB
    minor collections=4328  major collections=21 compactions=0


[Info] runtime: 00:03:00.472
[Info] vars: 1644, evals: 12730

[Info] |called|=84

Memory statistics: total=9543.86MB, max=27.65MB, minor=9541.45MB, major=112.21MB, promoted=109.81MB
    minor collections=4560  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)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi002_tso.i:861:3-861:42)

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

[Info] |called|=0

Memory statistics: total=10048.61MB, max=27.65MB, minor=10046.17MB, major=118.34MB, promoted=115.91MB
    minor collections=4801  major collections=22 compactions=0

[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][Witness] witness generation summary:
  total generation entries: 2
[Info][Race] Memory locations race summary:
  safe: 34
  vulnerable: 0
  unsafe: 0
  total memory locations: 34
