/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume graves-cpa/sumt8.yml.witness.yml --witness.yaml.validate graves-cpa/sumt8.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/sumt8.c


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )

runtime: 00:00:10.134
vars: 55, evals: 63

|rho|=55
|called|=3
|stable|=38
|infl|=52
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/sumt8.c:16:1-43:1
1	contexts for entry state of reach_error (1999) on ../plain/sumt8.c:3:1-3:71
1	contexts for entry state of __VERIFIER_assert (2006) on ../plain/sumt8.c:8:1-13:1

Memory statistics: total=107.48MB, max=12.37MB, minor=104.69MB, major=12.65MB, promoted=9.85MB
    minor collections=70  major collections=5 compactions=0


runtime: 00:00:20.128
vars: 61, evals: 109

|rho|=61
|called|=3
|stable|=61
|infl|=58
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/sumt8.c:16:1-43:1
1	contexts for entry state of reach_error (1999) on ../plain/sumt8.c:3:1-3:71
1	contexts for entry state of __VERIFIER_assert (2006) on ../plain/sumt8.c:8:1-13:1

Memory statistics: total=195.22MB, max=12.37MB, minor=192.42MB, major=17.86MB, promoted=15.06MB
    minor collections=137  major collections=7 compactions=0

[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt8.c:19:3-19:30)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt8.c:20:7-20:19)
[Info][Witness] unassume invariant: ((((((((((((((! (l == 0U) && ! (l == 1U)) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ((((((((((! (v4 == l) && ! (v5 == 0U)) && v4 == 0U) && (((((((((v1 == 0U && v2 == 0U) && v3 == 0U) && v5 == 1U) && ! (v5 == l)) && ! (j == 0U)) || (((((j == 0U && v2 == 0U) && v3 == 0U) && v5 == 1U) && ! (v5 == l)) && ! (v1 == 0U))) || (((((j == 0U && v1 == 0U) && v3 == 0U) && v5 == 1U) && ! (v5 == l)) && ! (v2 == 0U))) || (((((v2 == 0U && j == 0U) && v1 == 0U) && v5 == 1U) && ! (v5 == l)) && ! (v3 == 0U))) || (((((v2 == 0U && j == 0U) && v1 == 0U) && v3 == 0U) && v5 == l) && ! (v5 == 1U)))) && k == 0U) || ((! (k == 0U) && ((((((((((((((((((! (v5 == l) && ! (v4 == l)) && ((! (v5 == 1U) && v5 == 0U) || ! (v5 == 0U))) && v4 == 0U) || (((! (v5 == 0U) && ! (v4 == 0U)) && ! (v5 == l)) && v4 == l)) || ((((! (v5 == 0U) && ! (v4 == 0U)) && ! (v4 == l)) && ! (v5 == 1U)) && v5 == l)) || (((! (v4 == l) && ! (v5 == 0U)) && ! (v4 == 0U)) && ! (v5 == l))) && v3 == 0U) || ((((! (v4 == l) && ! (v5 == 0U)) && ! (v3 == 0U)) && ((! (v5 == 1U) && v5 == l) || ! (v5 == l))) && v4 == 0U)) || ((((! (v3 == 0U) && ! (v4 == 0U)) && ! (v5 == 0U)) && v5 == 1U) && ! (v5 == l))) && v2 == 0U) || ((((((! (v2 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v3 == 0U))) || (((((! (v4 == l) && ! (v5 == 0U)) && v3 == 0U) && ! (v2 == 0U)) && ((! (v5 == 1U) && v5 == l) || ! (v5 == l))) && v4 == 0U)) || (((((! (v2 == 0U) && v3 == 0U) && ! (v4 == 0U)) && ! (v5 == 0U)) && v5 == 1U) && ! (v5 == l))) && v1 == 0U) || (((((((! (v1 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v2 == 0U))) || (((((((! (v1 == 0U) && v2 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v3 == 0U))) || ((((((! (v4 == l) && ! (v5 == 0U)) && v3 == 0U) && ! (v1 == 0U)) && v2 == 0U) && ((! (v5 == 1U) && v5 == l) || ! (v5 == l))) && v4 == 0U)) || ((((((! (v1 == 0U) && v2 == 0U) && v3 == 0U) && ! (v4 == 0U)) && ! (v5 == 0U)) && v5 == 1U) && ! (v5 == l)))) && j == 0U)) || (((((((((! (j == 0U) && ! (k == 0U)) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v1 == 0U))) || (((((((((v1 == 0U && ! (k == 0U)) && ! (j == 0U)) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v2 == 0U))) || (((((((((v2 == 0U && v1 == 0U) && ! (k == 0U)) && ! (j == 0U)) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v3 == 0U))) || ((((((((! (k == 0U) && ! (j == 0U)) && v1 == 0U) && ! (v4 == l)) && ! (v5 == 0U)) && v3 == 0U) && v2 == 0U) && ((! (v5 == 1U) && v5 == l) || ! (v5 == l))) && v4 == 0U)) || ((((((((v2 == 0U && v1 == 0U) && ! (k == 0U)) && ! (j == 0U)) && v3 == 0U) && ! (v4 == 0U)) && ! (v5 == 0U)) && v5 == 1U) && ! (v5 == l)))) && i == 0U) || (((((((((((((! (i == 0U) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && k == 0U)) || (((((((((((((! (k == 0U) && ! (i == 0U)) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (j == 0U))) || (((((((((((((! (k == 0U) && ! (i == 0U)) && j == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (v1 == 0U))) || (((((((((((((v1 == 0U && ! (k == 0U)) && ! (i == 0U)) && j == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (v2 == 0U))) || (((((((((((((v2 == 0U && v1 == 0U) && ! (k == 0U)) && ! (i == 0U)) && j == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (v3 == 0U))) || ((((((((((((! (k == 0U) && j == 0U) && ! (l == 0U)) && ! (i == 0U)) && v1 == 0U) && ! (v4 == l)) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v5 == 0U)) && v3 == 0U) && v2 == 0U) && ! (l == 1U)) && ((! (v5 == 1U) && v5 == l) || ! (v5 == l))) && v4 == 0U)) || ((((((((((((v2 == 0U && v1 == 0U) && ! (k == 0U)) && ! (i == 0U)) && j == 0U) && v3 == 0U) && ! (v4 == 0U)) && ! (v5 == 0U)) && ! (l == 0U)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l))) || (((((((((((((i == 0U && k == 0U) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && v5 == 0U) && l == 0U) && v4 == l) && v5 == l) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == 1U))) || ((((((((((((((k == 0U && i == 0U) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (k == 0U))) || (((((((((((((i == 0U && k == 0U) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && v5 == l) && v5 == 1U) && l == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v4 == l))) || ((((((((((((((v5 == l && ! (i == 0U)) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (k == 0U)) (../plain/sumt8.c:20:7-20:19)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt8.c:23:7-23:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:23:7-23:13)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt8.c:23:7-23:13)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt8.c:25:12-25:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:25:12-25:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt8.c:25:12-25:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt8.c:27:12-27:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:27:12-27:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt8.c:27:12-27:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt8.c:29:12-29:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:29:12-29:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt8.c:29:12-29:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt8.c:31:12-31:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:31:12-31:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt8.c:31:12-31:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt8.c:33:12-33:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:33:12-33:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt8.c:33:12-33:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt8.c:35:12-35:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:35:12-35:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt8.c:35:12-35:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:38:6-38:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:36:5-36:12)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:34:6-34:15)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:32:6-32:17)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:30:6-30:17)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:28:6-28:17)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:26:6-26:17)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:24:6-24:17)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt8.c:40:5-40:51)
[Info][Witness] unassume invariant: ((((((((((((((! (l == 0U) && ! (l == 1U)) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ((((((((((! (v4 == l) && ! (v5 == 0U)) && v4 == 0U) && (((((((((v1 == 0U && v2 == 0U) && v3 == 0U) && v5 == 1U) && ! (v5 == l)) && ! (j == 0U)) || (((((j == 0U && v2 == 0U) && v3 == 0U) && v5 == 1U) && ! (v5 == l)) && ! (v1 == 0U))) || (((((j == 0U && v1 == 0U) && v3 == 0U) && v5 == 1U) && ! (v5 == l)) && ! (v2 == 0U))) || (((((v2 == 0U && j == 0U) && v1 == 0U) && v5 == 1U) && ! (v5 == l)) && ! (v3 == 0U))) || (((((v2 == 0U && j == 0U) && v1 == 0U) && v3 == 0U) && v5 == l) && ! (v5 == 1U)))) && k == 0U) || ((! (k == 0U) && ((((((((((((((((((! (v5 == l) && ! (v4 == l)) && ((! (v5 == 1U) && v5 == 0U) || ! (v5 == 0U))) && v4 == 0U) || (((! (v5 == 0U) && ! (v4 == 0U)) && ! (v5 == l)) && v4 == l)) || ((((! (v5 == 0U) && ! (v4 == 0U)) && ! (v4 == l)) && ! (v5 == 1U)) && v5 == l)) || (((! (v4 == l) && ! (v5 == 0U)) && ! (v4 == 0U)) && ! (v5 == l))) && v3 == 0U) || ((((! (v4 == l) && ! (v5 == 0U)) && ! (v3 == 0U)) && ((! (v5 == 1U) && v5 == l) || ! (v5 == l))) && v4 == 0U)) || ((((! (v3 == 0U) && ! (v4 == 0U)) && ! (v5 == 0U)) && v5 == 1U) && ! (v5 == l))) && v2 == 0U) || ((((((! (v2 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v3 == 0U))) || (((((! (v4 == l) && ! (v5 == 0U)) && v3 == 0U) && ! (v2 == 0U)) && ((! (v5 == 1U) && v5 == l) || ! (v5 == l))) && v4 == 0U)) || (((((! (v2 == 0U) && v3 == 0U) && ! (v4 == 0U)) && ! (v5 == 0U)) && v5 == 1U) && ! (v5 == l))) && v1 == 0U) || (((((((! (v1 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v2 == 0U))) || (((((((! (v1 == 0U) && v2 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v3 == 0U))) || ((((((! (v4 == l) && ! (v5 == 0U)) && v3 == 0U) && ! (v1 == 0U)) && v2 == 0U) && ((! (v5 == 1U) && v5 == l) || ! (v5 == l))) && v4 == 0U)) || ((((((! (v1 == 0U) && v2 == 0U) && v3 == 0U) && ! (v4 == 0U)) && ! (v5 == 0U)) && v5 == 1U) && ! (v5 == l)))) && j == 0U)) || (((((((((! (j == 0U) && ! (k == 0U)) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v1 == 0U))) || (((((((((v1 == 0U && ! (k == 0U)) && ! (j == 0U)) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v2 == 0U))) || (((((((((v2 == 0U && v1 == 0U) && ! (k == 0U)) && ! (j == 0U)) && v4 == 0U) && ! (v5 == 0U)) && ! (v4 == l)) && v5 == 1U) && ! (v5 == l)) && ! (v3 == 0U))) || ((((((((! (k == 0U) && ! (j == 0U)) && v1 == 0U) && ! (v4 == l)) && ! (v5 == 0U)) && v3 == 0U) && v2 == 0U) && ((! (v5 == 1U) && v5 == l) || ! (v5 == l))) && v4 == 0U)) || ((((((((v2 == 0U && v1 == 0U) && ! (k == 0U)) && ! (j == 0U)) && v3 == 0U) && ! (v4 == 0U)) && ! (v5 == 0U)) && v5 == 1U) && ! (v5 == l)))) && i == 0U) || (((((((((((((! (i == 0U) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && k == 0U)) || (((((((((((((! (k == 0U) && ! (i == 0U)) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (j == 0U))) || (((((((((((((! (k == 0U) && ! (i == 0U)) && j == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (v1 == 0U))) || (((((((((((((v1 == 0U && ! (k == 0U)) && ! (i == 0U)) && j == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (v2 == 0U))) || (((((((((((((v2 == 0U && v1 == 0U) && ! (k == 0U)) && ! (i == 0U)) && j == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (v3 == 0U))) || ((((((((((((! (k == 0U) && j == 0U) && ! (l == 0U)) && ! (i == 0U)) && v1 == 0U) && ! (v4 == l)) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v5 == 0U)) && v3 == 0U) && v2 == 0U) && ! (l == 1U)) && ((! (v5 == 1U) && v5 == l) || ! (v5 == l))) && v4 == 0U)) || ((((((((((((v2 == 0U && v1 == 0U) && ! (k == 0U)) && ! (i == 0U)) && j == 0U) && v3 == 0U) && ! (v4 == 0U)) && ! (v5 == 0U)) && ! (l == 0U)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l))) || (((((((((((((i == 0U && k == 0U) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && v5 == 0U) && l == 0U) && v4 == l) && v5 == l) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == 1U))) || ((((((((((((((k == 0U && i == 0U) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (k == 0U))) || (((((((((((((i == 0U && k == 0U) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && v5 == l) && v5 == 1U) && l == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v4 == l))) || ((((((((((((((v5 == l && ! (i == 0U)) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (v5 == 0U)) && ! (l == 0U)) && ! (v4 == l)) && v5 == 1U) && l == v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (l == 1U)) && ! (v5 == l)) && ! (k == 0U)) (../plain/sumt8.c:40:5-40:51)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/sumt8.c:5:1-7:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 30
  dead: 2 (2 in uncalled functions)
  total lines: 32
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow
[Warning][Witness] invariant unconfirmed: (!(l == (0)) && !(l == (1)) && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ((!(v4 == l) && !(v5 == (0)) && v4 == (0) && ((v1 == (0) && v2 == (0) && v3 == (0) && v5 == (1) && !(v5 == l) && !(j == (0))) || (j == (0) && v2 == (0) && v3 == (0) && v5 == (1) && !(v5 == l) && !(v1 == (0))) || (j == (0) && v1 == (0) && v3 == (0) && v5 == (1) && !(v5 == l) && !(v2 == (0))) || (v2 == (0) && j == (0) && v1 == (0) && v5 == (1) && !(v5 == l) && !(v3 == (0))) || (v2 == (0) && j == (0) && v1 == (0) && v3 == (0) && v5 == l && !(v5 == (1)))) && k == (0)) || (!(k == (0)) && ((((((((!(v5 == l) && !(v4 == l) && ((!(v5 == (1)) && v5 == (0)) || !(v5 == (0))) && v4 == (0)) || (!(v5 == (0)) && !(v4 == (0)) && !(v5 == l) && v4 == l) || (!(v5 == (0)) && !(v4 == (0)) && !(v4 == l) && !(v5 == (1)) && v5 == l) || (!(v4 == l) && !(v5 == (0)) && !(v4 == (0)) && !(v5 == l))) && v3 == (0)) || (!(v4 == l) && !(v5 == (0)) && !(v3 == (0)) && ((!(v5 == (1)) && v5 == l) || !(v5 == l)) && v4 == (0)) || (!(v3 == (0)) && !(v4 == (0)) && !(v5 == (0)) && v5 == (1) && !(v5 == l))) && v2 == (0)) || (!(v2 == (0)) && v4 == (0) && !(v5 == (0)) && !(v4 == l) && v5 == (1) && !(v5 == l) && !(v3 == (0))) || (!(v4 == l) && !(v5 == (0)) && v3 == (0) && !(v2 == (0)) && ((!(v5 == (1)) && v5 == l) || !(v5 == l)) && v4 == (0)) || (!(v2 == (0)) && v3 == (0) && !(v4 == (0)) && !(v5 == (0)) && v5 == (1) && !(v5 == l))) && v1 == (0)) || (!(v1 == (0)) && v3 == (0) && v4 == (0) && !(v5 == (0)) && !(v4 == l) && v5 == (1) && !(v5 == l) && !(v2 == (0))) || (!(v1 == (0)) && v2 == (0) && v4 == (0) && !(v5 == (0)) && !(v4 == l) && v5 == (1) && !(v5 == l) && !(v3 == (0))) || (!(v4 == l) && !(v5 == (0)) && v3 == (0) && !(v1 == (0)) && v2 == (0) && ((!(v5 == (1)) && v5 == l) || !(v5 == l)) && v4 == (0)) || (!(v1 == (0)) && v2 == (0) && v3 == (0) && !(v4 == (0)) && !(v5 == (0)) && v5 == (1) && !(v5 == l))) && j == (0)) || (!(j == (0)) && !(k == (0)) && v2 == (0) && v3 == (0) && v4 == (0) && !(v5 == (0)) && !(v4 == l) && v5 == (1) && !(v5 == l) && !(v1 == (0))) || (v1 == (0) && !(k == (0)) && !(j == (0)) && v3 == (0) && v4 == (0) && !(v5 == (0)) && !(v4 == l) && v5 == (1) && !(v5 == l) && !(v2 == (0))) || (v2 == (0) && v1 == (0) && !(k == (0)) && !(j == (0)) && v4 == (0) && !(v5 == (0)) && !(v4 == l) && v5 == (1) && !(v5 == l) && !(v3 == (0))) || (!(k == (0)) && !(j == (0)) && v1 == (0) && !(v4 == l) && !(v5 == (0)) && v3 == (0) && v2 == (0) && ((!(v5 == (1)) && v5 == l) || !(v5 == l)) && v4 == (0)) || (v2 == (0) && v1 == (0) && !(k == (0)) && !(j == (0)) && v3 == (0) && !(v4 == (0)) && !(v5 == (0)) && v5 == (1) && !(v5 == l))) && i == (0)) || (!(i == (0)) && j == (0) && v1 == (0) && v2 == (0) && v3 == (0) && v4 == (0) && !(v5 == (0)) && !(l == (0)) && !(v4 == l) && v5 == (1) && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(l == (1)) && !(v5 == l) && k == (0)) || (!(k == (0)) && !(i == (0)) && v1 == (0) && v2 == (0) && v3 == (0) && v4 == (0) && !(v5 == (0)) && !(l == (0)) && !(v4 == l) && v5 == (1) && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(l == (1)) && !(v5 == l) && !(j == (0))) || (!(k == (0)) && !(i == (0)) && j == (0) && v2 == (0) && v3 == (0) && v4 == (0) && !(v5 == (0)) && !(l == (0)) && !(v4 == l) && v5 == (1) && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(l == (1)) && !(v5 == l) && !(v1 == (0))) || (v1 == (0) && !(k == (0)) && !(i == (0)) && j == (0) && v3 == (0) && v4 == (0) && !(v5 == (0)) && !(l == (0)) && !(v4 == l) && v5 == (1) && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(l == (1)) && !(v5 == l) && !(v2 == (0))) || (v2 == (0) && v1 == (0) && !(k == (0)) && !(i == (0)) && j == (0) && v4 == (0) && !(v5 == (0)) && !(l == (0)) && !(v4 == l) && v5 == (1) && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(l == (1)) && !(v5 == l) && !(v3 == (0))) || (!(k == (0)) && j == (0) && !(l == (0)) && !(i == (0)) && v1 == (0) && !(v4 == l) && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v5 == (0)) && v3 == (0) && v2 == (0) && !(l == (1)) && ((!(v5 == (1)) && v5 == l) || !(v5 == l)) && v4 == (0)) || (v2 == (0) && v1 == (0) && !(k == (0)) && !(i == (0)) && j == (0) && v3 == (0) && !(v4 == (0)) && !(v5 == (0)) && !(l == (0)) && v5 == (1) && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(l == (1)) && !(v5 == l)) || (i == (0) && k == (0) && j == (0) && v1 == (0) && v2 == (0) && v3 == (0) && v4 == (0) && v5 == (0) && l == (0) && v4 == l && v5 == l && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(l == (1)) && !(v5 == (1))) || (k == (0) && i == (0) && j == (0) && v1 == (0) && v2 == (0) && v3 == (0) && v4 == (0) && !(v5 == (0)) && !(l == (0)) && !(v4 == l) && v5 == (1) && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(l == (1)) && !(v5 == l) && !(k == (0))) || (i == (0) && k == (0) && j == (0) && v1 == (0) && v2 == (0) && v3 == (0) && v4 == (0) && !(v5 == (0)) && !(l == (0)) && v5 == l && v5 == (1) && l == (1) && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v4 == l)) || (v5 == l && !(i == (0)) && j == (0) && v1 == (0) && v2 == (0) && v3 == (0) && v4 == (0) && !(v5 == (0)) && !(l == (0)) && !(v4 == l) && v5 == (1) && l == (v5 + (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(l == (1)) && !(v5 == l) && !(k == (0))) (../plain/sumt8.c:21:3)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 1
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: unknown

vars = 61    evals = 127    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                           29.575s    29.576s    331.41MB      1×
  preprocess                         0.023s     0.022s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.16MB      4×
  Cabs2cil                           0.005s     0.005s      4.80MB      4×
  mergeCIL                           0.003s     0.003s      3.35MB      1×
  analysis                          29.536s    29.537s    314.10MB      1×
    createCFG                          0.001s     0.001s      0.67MB      1×
      handle                             0.001s     0.001s      0.11MB     34×
      iter_connect                       0.001s     0.001s      0.44MB     34×
        computeSCCs                        0.001s     0.001s      0.26MB     35×
    FrontC                             0.003s     0.003s      2.46MB      2×
    Cabs2cil                           0.005s     0.005s      2.35MB      2×
    global_inits                       0.001s     0.001s      0.18MB      1×
    solving                           27.297s    27.297s    244.57MB      1×
      S.Dom.equal                        0.001s     0.001s      0.05MB    128×
      base unassume                      0.225s     0.225s    159.21MB     11×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.099s     0.099s     17.38MB      1×
        postsolver_iter                    0.099s     0.099s     17.33MB      1×
    warn_global                        0.001s     0.001s      0.18MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
