./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/safe006_power.opt-thin000_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.152
[Info] vars: 699, evals: 1536

[Info] |called|=75

Memory statistics: total=919.23MB, max=13.74MB, minor=917.07MB, major=20.59MB, promoted=18.43MB
    minor collections=441  major collections=8 compactions=0


[Info] runtime: 00:00:20.174
[Info] vars: 714, evals: 2196

[Info] |called|=87

Memory statistics: total=1288.93MB, max=13.74MB, minor=1286.77MB, major=24.38MB, promoted=22.22MB
    minor collections=618  major collections=9 compactions=0


[Info] runtime: 00:00:30.193
[Info] vars: 781, evals: 2891

[Info] |called|=86

Memory statistics: total=1706.03MB, max=15.81MB, minor=1703.87MB, major=29.22MB, promoted=27.05MB
    minor collections=817  major collections=10 compactions=0


[Info] runtime: 00:00:40.208
[Info] vars: 807, evals: 3606

[Info] |called|=63

Memory statistics: total=2145.69MB, max=18.18MB, minor=2143.51MB, major=34.83MB, promoted=32.66MB
    minor collections=1027  major collections=11 compactions=0


[Info] runtime: 00:00:50.224
[Info] vars: 868, evals: 4442

[Info] |called|=82

Memory statistics: total=2650.32MB, max=18.18MB, minor=2648.15MB, major=40.57MB, promoted=38.39MB
    minor collections=1268  major collections=12 compactions=0


[Info] runtime: 00:01:00.240
[Info] vars: 907, evals: 5260

[Info] |called|=75

Memory statistics: total=3164.02MB, max=18.18MB, minor=3161.83MB, major=46.89MB, promoted=44.70MB
    minor collections=1514  major collections=13 compactions=0

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

[Info] runtime: 00:01:10.253
[Info] vars: 926, evals: 5949

[Info] |called|=0

Memory statistics: total=3723.29MB, max=18.18MB, minor=3721.08MB, major=52.94MB, promoted=50.73MB
    minor collections=1781  major collections=14 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe006_power.opt-thin000_power.opt.i:810:3-810:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe006_power.opt-thin000_power.opt.i:842:3-842:159)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe006_power.opt-thin000_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/safe006_power.opt-thin000_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/safe006_power.opt-thin000_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/safe006_power.opt-thin000_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/safe006_power.opt-thin000_power.opt.i:105:1-109:1)
[Warning][Deadcode] Function 'fence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe006_power.opt-thin000_power.opt.i:814:1-816:1)
[Warning][Deadcode] Function 'isync' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe006_power.opt-thin000_power.opt.i:817:1-819:1)
[Warning][Deadcode] Function 'lwfence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe006_power.opt-thin000_power.opt.i:820:1-822:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 87
  dead: 8 (8 in uncalled functions)
  total lines: 95
[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/safe006_power.opt-thin000_power.opt.i:806:3-806: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/safe006_power.opt-thin000_power.opt.i:788:3-788: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/safe006_power.opt-thin000_power.opt.i:807:3-807: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/safe006_power.opt-thin000_power.opt.i:788:3-788: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/safe006_power.opt-thin000_power.opt.i:807:3-807: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/safe006_power.opt-thin000_power.opt.i:788:3-788: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/safe006_power.opt-thin000_power.opt.i:788:3-788: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/safe006_power.opt-thin000_power.opt.i:788:3-788: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/safe006_power.opt-thin000_power.opt.i:788:3-788: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/safe006_power.opt-thin000_power.opt.i:788:3-788:306)
[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/safe006_power.opt-thin000_power.opt.i:834:3-834: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/safe006_power.opt-thin000_power.opt.i:834:3-834: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/safe006_power.opt-thin000_power.opt.i:789:3-789: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/safe006_power.opt-thin000_power.opt.i:789:3-789:350)
[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/safe006_power.opt-thin000_power.opt.i:835:3-835: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/safe006_power.opt-thin000_power.opt.i:789:3-789: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/safe006_power.opt-thin000_power.opt.i:789:3-789: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/safe006_power.opt-thin000_power.opt.i:789:3-789:350)
[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/safe006_power.opt-thin000_power.opt.i:836:3-836:116)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe006_power.opt-thin000_power.opt.i:17:73-17:74)
[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/safe006_power.opt-thin000_power.opt.i:836:3-836: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/safe006_power.opt-thin000_power.opt.i:789:3-789:350)
[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/safe006_power.opt-thin000_power.opt.i:837:3-837: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/safe006_power.opt-thin000_power.opt.i:789:3-789:350)
[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/safe006_power.opt-thin000_power.opt.i:838:3-838: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/safe006_power.opt-thin000_power.opt.i:838:3-838: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/safe006_power.opt-thin000_power.opt.i:760:3-760: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/safe006_power.opt-thin000_power.opt.i:790:3-790: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/safe006_power.opt-thin000_power.opt.i:790:3-790: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/safe006_power.opt-thin000_power.opt.i:790:3-790: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/safe006_power.opt-thin000_power.opt.i:790:3-790: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/safe006_power.opt-thin000_power.opt.i:790:3-790:322)
[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/safe006_power.opt-thin000_power.opt.i:767:3-767: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/safe006_power.opt-thin000_power.opt.i:790:3-790: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/safe006_power.opt-thin000_power.opt.i:767:3-767: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/safe006_power.opt-thin000_power.opt.i:790:3-790:322)
[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/safe006_power.opt-thin000_power.opt.i:768:3-768:80)
[Warning][Deadcode][CWE-570] condition 'x$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe006_power.opt-thin000_power.opt.i:769:3-769: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/safe006_power.opt-thin000_power.opt.i:769:3-769: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/safe006_power.opt-thin000_power.opt.i:791:3-791: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/safe006_power.opt-thin000_power.opt.i:791:3-791:323)
[Warning][Deadcode][CWE-570] condition 'x$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe006_power.opt-thin000_power.opt.i:770:3-770: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/safe006_power.opt-thin000_power.opt.i:791:3-791: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/safe006_power.opt-thin000_power.opt.i:791:3-791: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/safe006_power.opt-thin000_power.opt.i:791:3-791:323)
[Warning][Deadcode][CWE-570] condition 'x$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe006_power.opt-thin000_power.opt.i:771:3-771: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/safe006_power.opt-thin000_power.opt.i:771:3-771: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/safe006_power.opt-thin000_power.opt.i:791:3-791: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/safe006_power.opt-thin000_power.opt.i:791:3-791: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/safe006_power.opt-thin000_power.opt.i:786:3-786: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/safe006_power.opt-thin000_power.opt.i:786:3-786: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/safe006_power.opt-thin000_power.opt.i:792:3-792: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/safe006_power.opt-thin000_power.opt.i:792:3-792: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/safe006_power.opt-thin000_power.opt.i:786:3-786: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/safe006_power.opt-thin000_power.opt.i:786:3-786: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/safe006_power.opt-thin000_power.opt.i:786:3-786: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/safe006_power.opt-thin000_power.opt.i:792:3-792: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/safe006_power.opt-thin000_power.opt.i:792:3-792: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/safe006_power.opt-thin000_power.opt.i:792:3-792: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/safe006_power.opt-thin000_power.opt.i:792:3-792: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/safe006_power.opt-thin000_power.opt.i:792:3-792: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/safe006_power.opt-thin000_power.opt.i:786:3-786: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/safe006_power.opt-thin000_power.opt.i:786:3-786: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/safe006_power.opt-thin000_power.opt.i:787:3-787: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/safe006_power.opt-thin000_power.opt.i:803:3-803: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/safe006_power.opt-thin000_power.opt.i:787:3-787: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/safe006_power.opt-thin000_power.opt.i:803:3-803: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/safe006_power.opt-thin000_power.opt.i:787:3-787: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/safe006_power.opt-thin000_power.opt.i:787:3-787: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/safe006_power.opt-thin000_power.opt.i:787:3-787: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/safe006_power.opt-thin000_power.opt.i:787:3-787: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/safe006_power.opt-thin000_power.opt.i:804:3-804: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/safe006_power.opt-thin000_power.opt.i:787:3-787: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/safe006_power.opt-thin000_power.opt.i:805:3-805: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/safe006_power.opt-thin000_power.opt.i:805:3-805:116)
SV-COMP result: unknown

[Info] runtime: 00:01:20.283
[Info] vars: 926, evals: 5949

[Info] |called|=0

Memory statistics: total=9893.06MB, max=24.04MB, minor=9890.42MB, major=78.35MB, promoted=75.70MB
    minor collections=4732  major collections=19 compactions=0

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