./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/safe000_power.opt.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.129
[Info] vars: 663, evals: 1430

[Info] |called|=81

Memory statistics: total=885.34MB, max=13.74MB, minor=883.18MB, major=20.82MB, promoted=18.67MB
    minor collections=425  major collections=8 compactions=0


[Info] runtime: 00:00:20.155
[Info] vars: 730, evals: 1909

[Info] |called|=91

Memory statistics: total=1158.68MB, max=15.81MB, minor=1156.52MB, major=23.29MB, promoted=21.13MB
    minor collections=555  major collections=9 compactions=0


[Info] runtime: 00:00:30.181
[Info] vars: 744, evals: 2373

[Info] |called|=78

Memory statistics: total=1436.83MB, max=15.81MB, minor=1434.67MB, major=26.35MB, promoted=24.19MB
    minor collections=688  major collections=9 compactions=0


[Info] runtime: 00:00:40.195
[Info] vars: 785, evals: 2841

[Info] |called|=77

Memory statistics: total=1723.27MB, max=15.81MB, minor=1721.11MB, major=29.67MB, promoted=27.51MB
    minor collections=825  major collections=10 compactions=0


[Info] runtime: 00:00:50.213
[Info] vars: 897, evals: 3554

[Info] |called|=79

Memory statistics: total=2173.77MB, max=18.18MB, minor=2171.59MB, major=36.35MB, promoted=34.17MB
    minor collections=1041  major collections=11 compactions=0


[Info] runtime: 00:01:00.238
[Info] vars: 923, evals: 4150

[Info] |called|=77

Memory statistics: total=2670.41MB, max=20.91MB, minor=2668.22MB, major=41.62MB, promoted=39.44MB
    minor collections=1278  major collections=12 compactions=0


[Info] runtime: 00:01:10.240
[Info] vars: 957, evals: 4790

[Info] |called|=73

Memory statistics: total=3090.20MB, max=20.91MB, minor=3088.01MB, major=46.83MB, promoted=44.64MB
    minor collections=1479  major collections=13 compactions=0


[Info] runtime: 00:01:20.259
[Info] vars: 1009, evals: 5479

[Info] |called|=85

Memory statistics: total=3520.55MB, max=20.91MB, minor=3518.35MB, major=51.78MB, promoted=49.59MB
    minor collections=1684  major collections=14 compactions=0


[Info] runtime: 00:01:30.266
[Info] vars: 1025, evals: 6143

[Info] |called|=74

Memory statistics: total=3978.96MB, max=20.91MB, minor=3976.75MB, major=57.04MB, promoted=54.82MB
    minor collections=1903  major collections=15 compactions=0


[Info] runtime: 00:01:40.285
[Info] vars: 1067, evals: 6764

[Info] |called|=55

Memory statistics: total=4380.58MB, max=20.91MB, minor=4378.32MB, major=62.05MB, promoted=59.79MB
    minor collections=2095  major collections=16 compactions=0

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

[Info] runtime: 00:01:50.302
[Info] vars: 1069, evals: 7194

[Info] |called|=0

Memory statistics: total=4834.60MB, max=20.91MB, minor=4832.31MB, major=67.04MB, promoted=64.75MB
    minor collections=2312  major collections=17 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:818:3-818:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:838:3-838:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:872:3-872:159)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:85:1-89:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:90:1-94:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:95:1-99:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:100:1-104:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:105:1-109:1)
[Warning][Deadcode] Function 'fence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:842:1-844:1)
[Warning][Deadcode] Function 'isync' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:845:1-847:1)
[Warning][Deadcode] Function 'lwfence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:848:1-850:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 107
  dead: 8 (8 in uncalled functions)
  total lines: 115
[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/safe000_power.opt.i:814:3-814: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/safe000_power.opt.i:796:3-796:306)
[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/safe000_power.opt.i:815:3-815: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/safe000_power.opt.i:796:3-796:306)
[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/safe000_power.opt.i:815:3-815: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/safe000_power.opt.i:796:3-796:306)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:796:3-796:306)
[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/safe000_power.opt.i:796:3-796:306)
[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/safe000_power.opt.i:796:3-796:306)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:796:3-796:306)
[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/safe000_power.opt.i:831:3-831: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/safe000_power.opt.i:831:3-831: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/safe000_power.opt.i:797:3-797:350)
[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/safe000_power.opt.i:832:3-832: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/safe000_power.opt.i:797:3-797:350)
[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/safe000_power.opt.i:797:3-797:350)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:797:3-797:350)
[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/safe000_power.opt.i:797:3-797:350)
[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/safe000_power.opt.i:833:3-833: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/safe000_power.opt.i:833:3-833:116)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:17:73-17:74)
[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/safe000_power.opt.i:834:3-834: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/safe000_power.opt.i:797:3-797:350)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:797:3-797:350)
[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/safe000_power.opt.i:835:3-835: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/safe000_power.opt.i:835:3-835: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/safe000_power.opt.i:767:3-767: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/safe000_power.opt.i:798:3-798:322)
[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/safe000_power.opt.i:798:3-798:322)
[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/safe000_power.opt.i:798:3-798:322)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:798:3-798:322)
[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/safe000_power.opt.i:798:3-798:322)
[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/safe000_power.opt.i:864:3-864: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/safe000_power.opt.i:775:3-775: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/safe000_power.opt.i:864:3-864: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/safe000_power.opt.i:798:3-798:322)
[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/safe000_power.opt.i:775:3-775:104)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:798:3-798:322)
[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/safe000_power.opt.i:865:3-865:80)
[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/safe000_power.opt.i:776:3-776:80)
[Warning][Deadcode][CWE-570] condition 'x$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:777:3-777:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:866:3-866: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/safe000_power.opt.i:866:3-866: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/safe000_power.opt.i:777:3-777: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/safe000_power.opt.i:799:3-799:323)
[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/safe000_power.opt.i:799:3-799:323)
[Warning][Deadcode][CWE-570] condition 'x$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:778:3-778:80)
[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/safe000_power.opt.i:867:3-867: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/safe000_power.opt.i:799:3-799:323)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:799:3-799:323)
[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/safe000_power.opt.i:799:3-799:323)
[Warning][Deadcode][CWE-570] condition 'x$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:779:3-779:116)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:868:3-868: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/safe000_power.opt.i:868:3-868: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/safe000_power.opt.i:779:3-779: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/safe000_power.opt.i:799:3-799:323)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:799:3-799:323)
[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/safe000_power.opt.i:794:3-794:364)
[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/safe000_power.opt.i:794:3-794:364)
[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/safe000_power.opt.i:800:3-800:352)
[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/safe000_power.opt.i:800:3-800:352)
[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/safe000_power.opt.i:794:3-794:364)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:794:3-794:364)
[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/safe000_power.opt.i:794:3-794:364)
[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/safe000_power.opt.i:800:3-800:352)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:800:3-800:352)
[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/safe000_power.opt.i:800:3-800:352)
[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/safe000_power.opt.i:800:3-800:352)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:800:3-800:352)
[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/safe000_power.opt.i:794:3-794:364)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:794:3-794:364)
[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/safe000_power.opt.i:795:3-795:306)
[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/safe000_power.opt.i:811:3-811:104)
[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/safe000_power.opt.i:795:3-795:306)
[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/safe000_power.opt.i:811:3-811: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/safe000_power.opt.i:795:3-795:306)
[Warning][Deadcode][CWE-571] condition '! x$r_buff1_thd2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:795:3-795:306)
[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/safe000_power.opt.i:795:3-795:306)
[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/safe000_power.opt.i:795:3-795:306)
[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/safe000_power.opt.i:812:3-812:80)
[Warning][Deadcode][CWE-570] condition 'x$r_buff1_thd2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe000_power.opt.i:795:3-795:306)
[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/safe000_power.opt.i:813:3-813: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/safe000_power.opt.i:813:3-813:116)
SV-COMP result: unknown

[Info] runtime: 00:02:00.311
[Info] vars: 1069, evals: 7194

[Info] |called|=0

Memory statistics: total=11322.11MB, max=24.04MB, minor=11319.38MB, major=93.65MB, promoted=90.91MB
    minor collections=5414  major collections=21 compactions=0

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