./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/safe009_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.117
[Info] vars: 660, evals: 1452

[Info] |called|=84

Memory statistics: total=890.33MB, max=13.74MB, minor=888.18MB, major=21.02MB, promoted=18.86MB
    minor collections=427  major collections=8 compactions=0


[Info] runtime: 00:00:20.149
[Info] vars: 727, evals: 1945

[Info] |called|=83

Memory statistics: total=1166.68MB, max=13.74MB, minor=1164.52MB, major=23.52MB, promoted=21.37MB
    minor collections=559  major collections=9 compactions=0


[Info] runtime: 00:00:30.168
[Info] vars: 741, evals: 2427

[Info] |called|=77

Memory statistics: total=1459.87MB, max=15.81MB, minor=1457.71MB, major=26.73MB, promoted=24.57MB
    minor collections=699  major collections=9 compactions=0


[Info] runtime: 00:00:40.193
[Info] vars: 808, evals: 2992

[Info] |called|=90

Memory statistics: total=1802.94MB, max=18.18MB, minor=1800.78MB, major=31.03MB, promoted=28.87MB
    minor collections=863  major collections=10 compactions=0


[Info] runtime: 00:00:50.211
[Info] vars: 902, evals: 3654

[Info] |called|=88

Memory statistics: total=2216.08MB, max=18.18MB, minor=2213.90MB, major=37.08MB, promoted=34.90MB
    minor collections=1061  major collections=11 compactions=0


[Info] runtime: 00:01:00.225
[Info] vars: 941, evals: 4349

[Info] |called|=80

Memory statistics: total=2768.35MB, max=18.18MB, minor=2766.16MB, major=42.99MB, promoted=40.80MB
    minor collections=1325  major collections=13 compactions=0


[Info] runtime: 00:01:10.249
[Info] vars: 971, evals: 5011

[Info] |called|=87

Memory statistics: total=3185.58MB, max=18.18MB, minor=3183.39MB, major=47.88MB, promoted=45.69MB
    minor collections=1524  major collections=13 compactions=0


[Info] runtime: 00:01:20.262
[Info] vars: 1011, evals: 5631

[Info] |called|=51

Memory statistics: total=3603.00MB, max=20.91MB, minor=3600.81MB, major=53.01MB, promoted=50.81MB
    minor collections=1724  major collections=14 compactions=0


[Info] runtime: 00:01:30.276
[Info] vars: 1042, evals: 6330

[Info] |called|=74

Memory statistics: total=4040.84MB, max=20.91MB, minor=4038.61MB, major=58.26MB, promoted=56.02MB
    minor collections=1933  major collections=15 compactions=0


[Info] runtime: 00:01:40.297
[Info] vars: 1061, evals: 7045

[Info] |called|=76

Memory statistics: total=4502.72MB, max=20.91MB, minor=4500.48MB, major=63.11MB, promoted=60.87MB
    minor collections=2154  major collections=16 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.opt.i:780:3-780:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.opt.i:816:3-816:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.opt.i:833:3-833:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.opt.i:867:3-867:159)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_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/safe009_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/safe009_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/safe009_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/safe009_power.opt.i:105:1-109:1)
[Warning][Deadcode] Function 'fence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.opt.i:837:1-839:1)
[Warning][Deadcode] Function 'isync' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.opt.i:840:1-842:1)
[Warning][Deadcode] Function 'lwfence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.opt.i:843:1-845:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 104
  dead: 8 (8 in uncalled functions)
  total lines: 112
[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/safe009_power.opt.i:812:3-812: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/safe009_power.opt.i:794:3-794: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/safe009_power.opt.i:813:3-813: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/safe009_power.opt.i:794:3-794: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/safe009_power.opt.i:813:3-813: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/safe009_power.opt.i:794:3-794: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/safe009_power.opt.i:794:3-794: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/safe009_power.opt.i:794:3-794: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/safe009_power.opt.i:794:3-794: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/safe009_power.opt.i:794:3-794: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/safe009_power.opt.i:826:3-826: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/safe009_power.opt.i:826:3-826:104)
[Warning][Deadcode][CWE-570] condition 'x$r_buff0_thd3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.opt.i:827:3-827: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/safe009_power.opt.i:795:3-795:350)
[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/safe009_power.opt.i:795:3-795: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/safe009_power.opt.i:828:3-828: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/safe009_power.opt.i:795:3-795: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/safe009_power.opt.i:795:3-795: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/safe009_power.opt.i:795:3-795: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/safe009_power.opt.i:828:3-828:116)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_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/safe009_power.opt.i:829:3-829: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/safe009_power.opt.i:795:3-795: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/safe009_power.opt.i:795:3-795: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/safe009_power.opt.i:830:3-830: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/safe009_power.opt.i:830:3-830: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/safe009_power.opt.i:765:3-765: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/safe009_power.opt.i:796:3-796: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/safe009_power.opt.i:796:3-796: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/safe009_power.opt.i:796:3-796: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/safe009_power.opt.i:859:3-859:104)
[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/safe009_power.opt.i:796:3-796: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/safe009_power.opt.i:796:3-796: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/safe009_power.opt.i:859:3-859: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/safe009_power.opt.i:773:3-773: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/safe009_power.opt.i:796:3-796: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/safe009_power.opt.i:773:3-773: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/safe009_power.opt.i:796:3-796: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/safe009_power.opt.i:860:3-860: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/safe009_power.opt.i:774:3-774: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/safe009_power.opt.i:861:3-861:116)
[Warning][Deadcode][CWE-570] condition 'x$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.opt.i:775:3-775: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/safe009_power.opt.i:861:3-861: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/safe009_power.opt.i:775:3-775: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/safe009_power.opt.i:862:3-862: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/safe009_power.opt.i:797:3-797: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/safe009_power.opt.i:797:3-797:323)
[Warning][Deadcode][CWE-570] condition 'x$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.opt.i:776:3-776: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/safe009_power.opt.i:797:3-797: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/safe009_power.opt.i:797:3-797:323)
[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/safe009_power.opt.i:863:3-863: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/safe009_power.opt.i:797:3-797:323)
[Warning][Deadcode][CWE-570] condition 'x$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.opt.i:777:3-777: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/safe009_power.opt.i:863:3-863: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/safe009_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/safe009_power.opt.i:797:3-797: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/safe009_power.opt.i:797:3-797: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/safe009_power.opt.i:792:3-792: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/safe009_power.opt.i:792:3-792: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/safe009_power.opt.i:798:3-798: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/safe009_power.opt.i:798:3-798: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/safe009_power.opt.i:792:3-792: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/safe009_power.opt.i:792:3-792: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/safe009_power.opt.i:792:3-792: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/safe009_power.opt.i:798:3-798: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/safe009_power.opt.i:798:3-798: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/safe009_power.opt.i:798:3-798: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/safe009_power.opt.i:798:3-798: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/safe009_power.opt.i:798:3-798: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/safe009_power.opt.i:792:3-792: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/safe009_power.opt.i:792:3-792: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/safe009_power.opt.i:793:3-793: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/safe009_power.opt.i:809:3-809: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/safe009_power.opt.i:793:3-793: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/safe009_power.opt.i:809:3-809: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/safe009_power.opt.i:793:3-793: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/safe009_power.opt.i:793:3-793: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/safe009_power.opt.i:793:3-793: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/safe009_power.opt.i:793:3-793: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/safe009_power.opt.i:810:3-810: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/safe009_power.opt.i:793:3-793: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/safe009_power.opt.i:811:3-811: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/safe009_power.opt.i:811:3-811:116)
SV-COMP result: unknown

[Info] runtime: 00:01:50.310
[Info] vars: 1061, evals: 7134

[Info] |called|=0

Memory statistics: total=6371.64MB, max=20.91MB, minor=6369.18MB, major=73.85MB, promoted=71.39MB
    minor collections=3049  major collections=18 compactions=0


[Info] runtime: 00:02:00.321
[Info] vars: 1061, evals: 7134

[Info] |called|=0

Memory statistics: total=13851.90MB, max=24.04MB, minor=13849.01MB, major=102.45MB, promoted=99.56MB
    minor collections=6630  major collections=22 compactions=0

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