./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/safe014_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.128
[Info] vars: 393, evals: 1540

[Info] |called|=59

Memory statistics: total=364.50MB, max=10.39MB, minor=362.38MB, major=12.62MB, promoted=10.50MB
    minor collections=175  major collections=6 compactions=0


[Info] runtime: 00:00:20.149
[Info] vars: 456, evals: 2983

[Info] |called|=75

Memory statistics: total=735.78MB, max=13.74MB, minor=733.66MB, major=18.32MB, promoted=16.20MB
    minor collections=352  major collections=7 compactions=0


[Info] runtime: 00:00:30.172
[Info] vars: 551, evals: 4454

[Info] |called|=67

Memory statistics: total=1147.74MB, max=15.81MB, minor=1145.59MB, major=24.84MB, promoted=22.69MB
    minor collections=550  major collections=9 compactions=0


[Info] runtime: 00:00:40.183
[Info] vars: 815, evals: 5556

[Info] |called|=63

Memory statistics: total=1751.64MB, max=15.81MB, minor=1749.47MB, major=33.82MB, promoted=31.65MB
    minor collections=839  major collections=11 compactions=0


[Info] runtime: 00:00:50.202
[Info] vars: 853, evals: 6252

[Info] |called|=66

Memory statistics: total=2349.85MB, max=18.18MB, minor=2347.67MB, major=40.36MB, promoted=38.18MB
    minor collections=1124  major collections=12 compactions=0


[Info] runtime: 00:01:00.212
[Info] vars: 914, evals: 7043

[Info] |called|=68

Memory statistics: total=2885.11MB, max=20.91MB, minor=2882.93MB, major=46.64MB, promoted=44.46MB
    minor collections=1380  major collections=13 compactions=0


[Info] runtime: 00:01:10.231
[Info] vars: 955, evals: 7832

[Info] |called|=69

Memory statistics: total=3412.22MB, max=20.91MB, minor=3410.03MB, major=53.34MB, promoted=51.14MB
    minor collections=1632  major collections=14 compactions=0


[Info] runtime: 00:01:20.240
[Info] vars: 987, evals: 8614

[Info] |called|=21

Memory statistics: total=3974.37MB, max=20.91MB, minor=3972.17MB, major=59.77MB, promoted=57.57MB
    minor collections=1901  major collections=16 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:785:3-785:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:800:3-800:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:829:3-829:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:863:3-863:159)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:86:1-90:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:91:1-95:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:96:1-100:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:101:1-105:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:106:1-110:1)
[Warning][Deadcode] Function 'fence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:833:1-835:1)
[Warning][Deadcode] Function 'isync' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:836:1-838:1)
[Warning][Deadcode] Function 'lwfence' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:839:1-841:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 97
  dead: 8 (8 in uncalled functions)
  total lines: 105
[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/safe014_power.opt.i:855:3-855: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/safe014_power.opt.i:770:3-770:322)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:770:3-770:322)
[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/safe014_power.opt.i:856:3-856:80)
[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/safe014_power.opt.i:770:3-770:322)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:770:3-770:322)
[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/safe014_power.opt.i:770:3-770:322)
[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/safe014_power.opt.i:857:3-857: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/safe014_power.opt.i:857:3-857:116)
[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/safe014_power.opt.i:770:3-770:322)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:770:3-770:322)
[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/safe014_power.opt.i:858:3-858:80)
[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/safe014_power.opt.i:859:3-859: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/safe014_power.opt.i:859:3-859:116)
[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/safe014_power.opt.i:771:3-771:323)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:771:3-771:323)
[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/safe014_power.opt.i:771:3-771:323)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:771:3-771:323)
[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/safe014_power.opt.i:771:3-771:323)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:18:73-18:74)
[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/safe014_power.opt.i:771:3-771:323)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:771:3-771:323)
[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/safe014_power.opt.i:766:3-766:364)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:766:3-766:364)
[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/safe014_power.opt.i:772:3-772:352)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:772:3-772:352)
[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/safe014_power.opt.i:766:3-766:364)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:766:3-766:364)
[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/safe014_power.opt.i:766:3-766:364)
[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/safe014_power.opt.i:772:3-772:352)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:772:3-772:352)
[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/safe014_power.opt.i:772:3-772:352)
[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/safe014_power.opt.i:772:3-772:352)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:772:3-772:352)
[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/safe014_power.opt.i:766:3-766:364)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:766:3-766:364)
[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/safe014_power.opt.i:767:3-767:306)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:767:3-767:306)
[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/safe014_power.opt.i:767:3-767:306)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:767:3-767:306)
[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/safe014_power.opt.i:767:3-767:306)
[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/safe014_power.opt.i:767:3-767:306)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:767:3-767:306)
[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/safe014_power.opt.i:814:3-814:57)
[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/safe014_power.opt.i:768:3-768:306)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:768:3-768:306)
[Warning][Deadcode][CWE-571] condition 'y$r_buff0_thd3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:822:3-822: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/safe014_power.opt.i:768:3-768:306)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:768:3-768:306)
[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/safe014_power.opt.i:768:3-768:306)
[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/safe014_power.opt.i:822:3-822: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/safe014_power.opt.i:768:3-768:306)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:768:3-768:306)
[Warning][Deadcode][CWE-571] condition 'y$r_buff0_thd3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:823:3-823:80)
[Warning][Deadcode][CWE-570] condition 'y$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:824:3-824: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/safe014_power.opt.i:824:3-824:116)
[Warning][Deadcode][CWE-570] condition 'y$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:825:3-825:80)
[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/safe014_power.opt.i:769:3-769:350)
[Warning][Deadcode][CWE-570] condition 'y$r_buff0_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:769:3-769:350)
[Warning][Deadcode][CWE-570] condition 'y$w_buff0_used' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:826:3-826:116)
[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/safe014_power.opt.i:769:3-769:350)
[Warning][Deadcode][CWE-571] condition '! y$r_buff1_thd1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:769:3-769:350)
[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/safe014_power.opt.i:769:3-769:350)
[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/safe014_power.opt.i:826:3-826:116)
[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/safe014_power.opt.i:769:3-769:350)
[Warning][Deadcode][CWE-570] condition 'y$r_buff1_thd1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe014_power.opt.i:769:3-769:350)
[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/safe014_power.opt.i:855:3-855:104)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 2
[Info][Race] Memory locations race summary:
  safe: 27
  vulnerable: 0
  unsafe: 0
  total memory locations: 27
