./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/weaver/chl-poker-hand-subst.wvr.c


--------------------------------------------------------------------------------


[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 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:57:5-64:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:86:5-92:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:142:5-149:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:170:5-176:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:226:5-233:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:254:5-260:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3-356:3 with factor 8
[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] malloc wrapper: create_fresh_int_array
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )

[Info] runtime: 00:00:10.145
[Info] vars: 1733, evals: 11866

[Info] |called|=32

Memory statistics: total=4794.13MB, max=20.91MB, minor=4791.69MB, major=49.12MB, promoted=46.68MB
    minor collections=2290  major collections=12 compactions=0


[Info] runtime: 00:00:20.190
[Info] vars: 2658, evals: 13758

[Info] |called|=30

Memory statistics: total=6805.21MB, max=27.65MB, minor=6802.64MB, major=69.16MB, promoted=66.60MB
    minor collections=3251  major collections=15 compactions=0


[Info] runtime: 00:00:30.219
[Info] vars: 3286, evals: 15443

[Info] |called|=30

Memory statistics: total=8677.21MB, max=31.80MB, minor=8674.61MB, major=86.76MB, promoted=84.16MB
    minor collections=4144  major collections=17 compactions=0


[Info] runtime: 00:00:40.246
[Info] vars: 3582, evals: 17116

[Info] |called|=28

Memory statistics: total=10624.17MB, max=36.57MB, minor=10621.56MB, major=104.55MB, promoted=101.94MB
    minor collections=5074  major collections=19 compactions=0


[Info] runtime: 00:00:50.274
[Info] vars: 3586, evals: 18671

[Info] |called|=38

Memory statistics: total=12501.20MB, max=36.57MB, minor=12498.59MB, major=120.49MB, promoted=117.88MB
    minor collections=5969  major collections=20 compactions=0

[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:363:10-363:15)

[Info] runtime: 00:01:00.292
[Info] vars: 3600, evals: 19813

[Info] |called|=0

Memory statistics: total=14473.80MB, max=42.06MB, minor=14471.11MB, major=138.76MB, promoted=136.08MB
    minor collections=6911  major collections=22 compactions=0

[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:346-346)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 266
  dead: 1
  total lines: 267
[Warning][Deadcode][CWE-571] condition 'i < size' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:7-354:32)
[Warning][Deadcode][CWE-571] condition 'i < size' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:7-354:32)
[Warning][Deadcode][CWE-571] condition 'i < size' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:7-354:32)
[Warning][Deadcode][CWE-571] condition 'i < size' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:7-354:32)
[Warning][Deadcode][CWE-571] condition 'i < size' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:7-354:32)
[Warning][Deadcode][CWE-571] condition 'i < size' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:7-354:32)
SV-COMP result: unknown

[Info] runtime: 00:01:10.307
[Info] vars: 3600, evals: 19813

[Info] |called|=0

Memory statistics: total=18497.79MB, max=55.63MB, minor=18494.66MB, major=172.20MB, promoted=169.07MB
    minor collections=8831  major collections=24 compactions=0

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