/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/sumt7.yml.witness.yml --witness.yaml.validate graves-cpa/sumt7.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/sumt7.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.098
vars: 57, evals: 101

|rho|=57
|called|=3
|stable|=42
|infl|=54
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=41
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 reach_error (1999) on ../plain/sumt7.c:3:1-3:71
1	contexts for entry state of __VERIFIER_assert (2006) on ../plain/sumt7.c:8:1-13:1
1	contexts for entry state of main (2011) on ../plain/sumt7.c:16:1-41:1

Memory statistics: total=267.07MB, max=14.22MB, minor=264.27MB, major=22.10MB, promoted=19.30MB
    minor collections=151  major collections=7 compactions=0

[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt7.c:19:3-19:30)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt7.c:20:7-20:19)
[Info][Witness] unassume invariant: ((((((((((((((((((((((i == 0U && j == 0U) && ! (v1 == 0U)) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (l == 0U)) && i == v2) && i == v3) && i == v4) && ! (i == l)) && v1 == 1U) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (l == 1U)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (k == 0U)) || ((((((((((((((((i == 0U && k == 0U) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && l == 0U) && i == v2) && i == v3) && i == v4) && v1 == l) && i == l) && v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (l == 1U)) && ! (v1 == 1U))) || ((((((((((((((((i == 0U && k == 0U) && j == 0U) && ! (v1 == 0U)) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (l == 0U)) && i == v2) && i == v3) && i == v4) && v1 == l) && v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && v1 == 1U) && l == 1U) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (i == l))) || (((((((((! (l == 1U) && ! (v1 == l)) && ! (k == 0U)) && ! (l == 0U)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == 0U)) && ! (i == l)) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && (((((i == v2 && (((i == v3 && (((! (v1 == 1U) && i == v4) && v4 == 0U) || ((! (v4 == 0U) && v1 == 1U) && ! (i == v4)))) && v3 == 0U) || ((((! (v3 == 0U) && v4 == 0U) && i == v4) && v1 == 1U) && ! (i == v3)))) && v2 == 0U) || ((((((! (v2 == 0U) && v3 == 0U) && v4 == 0U) && i == v3) && i == v4) && v1 == 1U) && ! (i == v2))) && j == 0U) || (((((((! (j == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && i == v2) && i == v3) && i == v4) && v1 == 1U))) && i == 0U)) || ((((((((((((((((! (i == 0U) && ! (k == 0U)) && j == 0U) && ! (v1 == 0U)) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (l == 0U)) && ! (i == l)) && v1 == 1U) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (l == 1U)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && ! (i == v3)) && ! (i == v2))) || (((((! (l == 1U) && ! (l == 0U)) && ! (i == l)) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ((((((((! (v1 == 0U) && (((((((((((((v2 == 0U && v3 == 0U) && v4 == 0U) && i == v2) && i == v3) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (j == 0U)) || (((((((((j == 0U && v3 == 0U) && v4 == 0U) && i == v3) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v2)) && ! (v2 == 0U))) || (((((((((v2 == 0U && j == 0U) && v4 == 0U) && i == v2) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v3)) && ! (v3 == 0U))) || (((((((((v3 == 0U && v2 == 0U) && j == 0U) && i == v2) && i == v3) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && ! (v4 == 0U))) || (((((((((v3 == 0U && v2 == 0U) && j == 0U) && v4 == 0U) && i == v2) && i == v3) && i == v4) && v1 == l) && v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (v1 == 1U)))) && k == 0U) || ((! (k == 0U) && ((((((((((((v2 == 0U && v3 == 0U) && v4 == 0U) && i == v2) && i == v3) && i == v4) && ! (v1 == l)) && ! (v1 == 1U)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && v1 == 0U) || (((i == v2 && ! (v1 == 0U)) && (((((((! (v1 == 1U) && i == v3) && ! (i == v4)) && ! (v4 == 0U)) && ((v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))) && v1 == l) || (! (v1 == l) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v3 == 0U) || (((((! (v1 == 1U) && ! (i == v3)) && i == v4) && ! (v3 == 0U)) && ((v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))) && v1 == l) || (! (v1 == l) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v4 == 0U)) || ((((((! (v3 == 0U) && ! (v4 == 0U)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && ! (i == v3)))) && v2 == 0U)) || (((((! (v2 == 0U) && ! (i == v2)) && i == v3) && ! (v1 == 0U)) && ((((! (v1 == 1U) && i == v4) && ((v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))) && v1 == l) || (! (v1 == l) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v4 == 0U) || ((((! (v4 == 0U) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)))) && v3 == 0U)) || (((((((((! (v1 == 0U) && ! (v2 == 0U)) && ! (v3 == 0U)) && v4 == 0U) && ! (i == v2)) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v3)))) && j == 0U)) || (((((((((((! (k == 0U) && ! (j == 0U)) && ! (v1 == 0U)) && v3 == 0U) && v4 == 0U) && i == v3) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v2)) && ! (v2 == 0U))) || (((((((((((! (k == 0U) && ! (j == 0U)) && ! (v1 == 0U)) && v2 == 0U) && v4 == 0U) && i == v2) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v3)) && ! (v3 == 0U))) || (((((((((((v3 == 0U && ! (k == 0U)) && ! (j == 0U)) && ! (v1 == 0U)) && v2 == 0U) && i == v2) && i == v3) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && ! (v4 == 0U))) || (((((((((((v3 == 0U && ! (k == 0U)) && ! (j == 0U)) && ! (v1 == 0U)) && v2 == 0U) && i == v2) && i == v3) && i == v4) && v4 == 0U) && v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (v1 == 1U)) && v1 == l)) || (((((((((((v3 == 0U && ! (v1 == 1U)) && ! (k == 0U)) && ! (j == 0U)) && ! (v1 == 0U)) && v2 == 0U) && i == v2) && i == v3) && i == v4) && v4 == 0U) && ! (v1 == l)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && i == 0U)) || (((((((! (l == 1U) && ! (k == 0U)) && ! (l == 0U)) && ! (i == 0U)) && ! (v1 == 0U)) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ((((! (i == v2) && ((((! (i == v3) && ((((! (i == v4) && ((((v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))) && ! (v1 == 1U)) && ! (i == l)) && v1 == l) || (((i == l || (! (i == l) && ! (v1 == 1U))) && ! (v1 == l)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v4 == 0U) || (((((! (v4 == 0U) && ! (i == l)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && i == v4)) || ((((! (v4 == 0U) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)))) && v3 == 0U) || (((((((! (v3 == 0U) && v4 == 0U) && ! (i == l)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && i == v3)) || ((((((v4 == 0U && ! (v3 == 0U)) && ! (i == v3)) && ! (i == v4)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)))) && v2 == 0U) || (((((((((! (v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (i == l)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && ! (i == v3)) && i == v2)) || ((((((((! (v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (i == v2)) && ! (i == v3)) && ! (i == v4)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)))) && j == 0U)) || (((((((((((((((! (i == 0U) && ! (k == 0U)) && ! (j == 0U)) && ! (v1 == 0U)) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (l == 0U)) && ! (i == v2)) && ! (i == v3)) && ! (i == v4)) && v1 == 1U) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (l == 1U)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) (../plain/sumt7.c:20:7-20:19)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt7.c:23:7-23:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:23:7-23:13)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt7.c:23:7-23:13)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt7.c:25:12-25:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:25:12-25:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt7.c:25:12-25:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt7.c:27:12-27:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:27:12-27:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt7.c:27:12-27:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt7.c:29:12-29:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:29:12-29:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt7.c:29:12-29:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt7.c:31:12-31:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:31:12-31:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt7.c:31:12-31:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/sumt7.c:33:12-33:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:33:12-33:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/sumt7.c:33:12-33:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:36:6-36:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:34:5-34:12)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:32:6-32:15)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:30:6-30:17)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:28:6-28:17)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:26:6-26:17)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:24:6-24:17)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/sumt7.c:38:5-38:48)
[Info][Witness] unassume invariant: ((((((((((((((((((((((i == 0U && j == 0U) && ! (v1 == 0U)) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (l == 0U)) && i == v2) && i == v3) && i == v4) && ! (i == l)) && v1 == 1U) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (l == 1U)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (k == 0U)) || ((((((((((((((((i == 0U && k == 0U) && j == 0U) && v1 == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && l == 0U) && i == v2) && i == v3) && i == v4) && v1 == l) && i == l) && v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (l == 1U)) && ! (v1 == 1U))) || ((((((((((((((((i == 0U && k == 0U) && j == 0U) && ! (v1 == 0U)) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (l == 0U)) && i == v2) && i == v3) && i == v4) && v1 == l) && v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && v1 == 1U) && l == 1U) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (i == l))) || (((((((((! (l == 1U) && ! (v1 == l)) && ! (k == 0U)) && ! (l == 0U)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == 0U)) && ! (i == l)) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && (((((i == v2 && (((i == v3 && (((! (v1 == 1U) && i == v4) && v4 == 0U) || ((! (v4 == 0U) && v1 == 1U) && ! (i == v4)))) && v3 == 0U) || ((((! (v3 == 0U) && v4 == 0U) && i == v4) && v1 == 1U) && ! (i == v3)))) && v2 == 0U) || ((((((! (v2 == 0U) && v3 == 0U) && v4 == 0U) && i == v3) && i == v4) && v1 == 1U) && ! (i == v2))) && j == 0U) || (((((((! (j == 0U) && v2 == 0U) && v3 == 0U) && v4 == 0U) && i == v2) && i == v3) && i == v4) && v1 == 1U))) && i == 0U)) || ((((((((((((((((! (i == 0U) && ! (k == 0U)) && j == 0U) && ! (v1 == 0U)) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (l == 0U)) && ! (i == l)) && v1 == 1U) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (l == 1U)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && ! (i == v3)) && ! (i == v2))) || (((((! (l == 1U) && ! (l == 0U)) && ! (i == l)) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ((((((((! (v1 == 0U) && (((((((((((((v2 == 0U && v3 == 0U) && v4 == 0U) && i == v2) && i == v3) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (j == 0U)) || (((((((((j == 0U && v3 == 0U) && v4 == 0U) && i == v3) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v2)) && ! (v2 == 0U))) || (((((((((v2 == 0U && j == 0U) && v4 == 0U) && i == v2) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v3)) && ! (v3 == 0U))) || (((((((((v3 == 0U && v2 == 0U) && j == 0U) && i == v2) && i == v3) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && ! (v4 == 0U))) || (((((((((v3 == 0U && v2 == 0U) && j == 0U) && v4 == 0U) && i == v2) && i == v3) && i == v4) && v1 == l) && v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (v1 == 1U)))) && k == 0U) || ((! (k == 0U) && ((((((((((((v2 == 0U && v3 == 0U) && v4 == 0U) && i == v2) && i == v3) && i == v4) && ! (v1 == l)) && ! (v1 == 1U)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && v1 == 0U) || (((i == v2 && ! (v1 == 0U)) && (((((((! (v1 == 1U) && i == v3) && ! (i == v4)) && ! (v4 == 0U)) && ((v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))) && v1 == l) || (! (v1 == l) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v3 == 0U) || (((((! (v1 == 1U) && ! (i == v3)) && i == v4) && ! (v3 == 0U)) && ((v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))) && v1 == l) || (! (v1 == l) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v4 == 0U)) || ((((((! (v3 == 0U) && ! (v4 == 0U)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && ! (i == v3)))) && v2 == 0U)) || (((((! (v2 == 0U) && ! (i == v2)) && i == v3) && ! (v1 == 0U)) && ((((! (v1 == 1U) && i == v4) && ((v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))) && v1 == l) || (! (v1 == l) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v4 == 0U) || ((((! (v4 == 0U) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)))) && v3 == 0U)) || (((((((((! (v1 == 0U) && ! (v2 == 0U)) && ! (v3 == 0U)) && v4 == 0U) && ! (i == v2)) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v3)))) && j == 0U)) || (((((((((((! (k == 0U) && ! (j == 0U)) && ! (v1 == 0U)) && v3 == 0U) && v4 == 0U) && i == v3) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v2)) && ! (v2 == 0U))) || (((((((((((! (k == 0U) && ! (j == 0U)) && ! (v1 == 0U)) && v2 == 0U) && v4 == 0U) && i == v2) && i == v4) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v3)) && ! (v3 == 0U))) || (((((((((((v3 == 0U && ! (k == 0U)) && ! (j == 0U)) && ! (v1 == 0U)) && v2 == 0U) && i == v2) && i == v3) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && ! (v4 == 0U))) || (((((((((((v3 == 0U && ! (k == 0U)) && ! (j == 0U)) && ! (v1 == 0U)) && v2 == 0U) && i == v2) && i == v3) && i == v4) && v4 == 0U) && v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (v1 == 1U)) && v1 == l)) || (((((((((((v3 == 0U && ! (v1 == 1U)) && ! (k == 0U)) && ! (j == 0U)) && ! (v1 == 0U)) && v2 == 0U) && i == v2) && i == v3) && i == v4) && v4 == 0U) && ! (v1 == l)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && i == 0U)) || (((((((! (l == 1U) && ! (k == 0U)) && ! (l == 0U)) && ! (i == 0U)) && ! (v1 == 0U)) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ((((! (i == v2) && ((((! (i == v3) && ((((! (i == v4) && ((((v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))) && ! (v1 == 1U)) && ! (i == l)) && v1 == l) || (((i == l || (! (i == l) && ! (v1 == 1U))) && ! (v1 == l)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v4 == 0U) || (((((! (v4 == 0U) && ! (i == l)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && i == v4)) || ((((! (v4 == 0U) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)))) && v3 == 0U) || (((((((! (v3 == 0U) && v4 == 0U) && ! (i == l)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && i == v3)) || ((((((v4 == 0U && ! (v3 == 0U)) && ! (i == v3)) && ! (i == v4)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)))) && v2 == 0U) || (((((((((! (v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (i == l)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) && ! (i == v4)) && ! (i == v3)) && i == v2)) || ((((((((! (v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (i == v2)) && ! (i == v3)) && ! (i == v4)) && v1 == 1U) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)))) && j == 0U)) || (((((((((((((((! (i == 0U) && ! (k == 0U)) && ! (j == 0U)) && ! (v1 == 0U)) && v2 == 0U) && v3 == 0U) && v4 == 0U) && ! (l == 0U)) && ! (i == v2)) && ! (i == v3)) && ! (i == v4)) && v1 == 1U) && l == v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ! (l == 1U)) && ! (v1 == v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && ! (v1 == l)) (../plain/sumt7.c:38:5-38:48)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/sumt7.c:5:1-7:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 28
  dead: 2 (2 in uncalled functions)
  total lines: 30
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow
[Warning][Witness] invariant unconfirmed: (i == (0) && j == (0) && !(v1 == (0)) && v2 == (0) && v3 == (0) && v4 == (0) && !(l == (0)) && i == v2 && i == v3 && i == v4 && !(i == l) && v1 == (1) && l == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && !(l == (1)) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(k == (0))) || (i == (0) && k == (0) && j == (0) && v1 == (0) && v2 == (0) && v3 == (0) && v4 == (0) && l == (0) && i == v2 && i == v3 && i == v4 && v1 == l && i == l && v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && l == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && !(l == (1)) && !(v1 == (1))) || (i == (0) && k == (0) && j == (0) && !(v1 == (0)) && v2 == (0) && v3 == (0) && v4 == (0) && !(l == (0)) && i == v2 && i == v3 && i == v4 && v1 == l && v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && v1 == (1) && l == (1) && l == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && !(i == l)) || (!(l == (1)) && !(v1 == l) && !(k == (0)) && !(l == (0)) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == (0)) && !(i == l) && l == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ((((i == v2 && ((i == v3 && ((!(v1 == (1)) && i == v4 && v4 == (0)) || (!(v4 == (0)) && v1 == (1) && !(i == v4))) && v3 == (0)) || (!(v3 == (0)) && v4 == (0) && i == v4 && v1 == (1) && !(i == v3))) && v2 == (0)) || (!(v2 == (0)) && v3 == (0) && v4 == (0) && i == v3 && i == v4 && v1 == (1) && !(i == v2))) && j == (0)) || (!(j == (0)) && v2 == (0) && v3 == (0) && v4 == (0) && i == v2 && i == v3 && i == v4 && v1 == (1))) && i == (0)) || (!(i == (0)) && !(k == (0)) && j == (0) && !(v1 == (0)) && v2 == (0) && v3 == (0) && v4 == (0) && !(l == (0)) && !(i == l) && v1 == (1) && l == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && !(l == (1)) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v4) && !(i == v3) && !(i == v2)) || (!(l == (1)) && !(l == (0)) && !(i == l) && l == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ((!(v1 == (0)) && ((v2 == (0) && v3 == (0) && v4 == (0) && i == v2 && i == v3 && i == v4 && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(j == (0))) || (j == (0) && v3 == (0) && v4 == (0) && i == v3 && i == v4 && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v2) && !(v2 == (0))) || (v2 == (0) && j == (0) && v4 == (0) && i == v2 && i == v4 && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v3) && !(v3 == (0))) || (v3 == (0) && v2 == (0) && j == (0) && i == v2 && i == v3 && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v4) && !(v4 == (0))) || (v3 == (0) && v2 == (0) && j == (0) && v4 == (0) && i == v2 && i == v3 && i == v4 && v1 == l && v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && !(v1 == (1)))) && k == (0)) || (!(k == (0)) && ((v2 == (0) && v3 == (0) && v4 == (0) && i == v2 && i == v3 && i == v4 && !(v1 == l) && !(v1 == (1)) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && v1 == (0)) || (i == v2 && !(v1 == (0)) && ((!(v1 == (1)) && i == v3 && !(i == v4) && !(v4 == (0)) && ((v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && v1 == l) || (!(v1 == l) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v3 == (0)) || (!(v1 == (1)) && !(i == v3) && i == v4 && !(v3 == (0)) && ((v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && v1 == l) || (!(v1 == l) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v4 == (0)) || (!(v3 == (0)) && !(v4 == (0)) && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v4) && !(i == v3))) && v2 == (0)) || (!(v2 == (0)) && !(i == v2) && i == v3 && !(v1 == (0)) && ((!(v1 == (1)) && i == v4 && ((v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && v1 == l) || (!(v1 == l) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v4 == (0)) || (!(v4 == (0)) && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v4))) && v3 == (0)) || (!(v1 == (0)) && !(v2 == (0)) && !(v3 == (0)) && v4 == (0) && !(i == v2) && i == v4 && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v3))) && j == (0)) || (!(k == (0)) && !(j == (0)) && !(v1 == (0)) && v3 == (0) && v4 == (0) && i == v3 && i == v4 && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v2) && !(v2 == (0))) || (!(k == (0)) && !(j == (0)) && !(v1 == (0)) && v2 == (0) && v4 == (0) && i == v2 && i == v4 && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v3) && !(v3 == (0))) || (v3 == (0) && !(k == (0)) && !(j == (0)) && !(v1 == (0)) && v2 == (0) && i == v2 && i == v3 && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v4) && !(v4 == (0))) || (v3 == (0) && !(k == (0)) && !(j == (0)) && !(v1 == (0)) && v2 == (0) && i == v2 && i == v3 && i == v4 && v4 == (0) && v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && !(v1 == (1)) && v1 == l) || (v3 == (0) && !(v1 == (1)) && !(k == (0)) && !(j == (0)) && !(v1 == (0)) && v2 == (0) && i == v2 && i == v3 && i == v4 && v4 == (0) && !(v1 == l) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && i == (0)) || (!(l == (1)) && !(k == (0)) && !(l == (0)) && !(i == (0)) && !(v1 == (0)) && l == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && ((!(i == v2) && ((!(i == v3) && ((!(i == v4) && ((v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && !(v1 == (1)) && !(i == l) && v1 == l) || ((i == l || (!(i == l) && !(v1 == (1)))) && !(v1 == l) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))))) && v4 == (0)) || (!(v4 == (0)) && !(i == l) && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && i == v4) || (!(v4 == (0)) && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v4))) && v3 == (0)) || (!(v3 == (0)) && v4 == (0) && !(i == l) && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v4) && i == v3) || (v4 == (0) && !(v3 == (0)) && !(i == v3) && !(i == v4) && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l))) && v2 == (0)) || (!(v2 == (0)) && v3 == (0) && v4 == (0) && !(i == l) && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l) && !(i == v4) && !(i == v3) && i == v2) || (!(v2 == (0)) && v3 == (0) && v4 == (0) && !(i == v2) && !(i == v3) && !(i == v4) && v1 == (1) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l))) && j == (0)) || (!(i == (0)) && !(k == (0)) && !(j == (0)) && !(v1 == (0)) && v2 == (0) && v3 == (0) && v4 == (0) && !(l == (0)) && !(i == v2) && !(i == v3) && !(i == v4) && v1 == (1) && l == (v4 + (v3 + (v2 + (v1 + (k + (i + j)))))) && !(l == (1)) && !(v1 == (v4 + (v3 + (v2 + (v1 + (k + (i + j))))))) && !(v1 == l)) (../plain/sumt7.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 = 57    evals = 116    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                           13.293s    13.294s    370.91MB      1×
  preprocess                         0.024s     0.023s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.15MB      4×
  Cabs2cil                           0.005s     0.005s      4.78MB      4×
  mergeCIL                           0.003s     0.003s      3.35MB      1×
  analysis                          13.252s    13.253s    353.65MB      1×
    createCFG                          0.001s     0.001s      0.66MB      1×
      handle                             0.001s     0.001s      0.11MB     34×
      iter_connect                       0.001s     0.001s      0.43MB     34×
        computeSCCs                        0.001s     0.001s      0.26MB     35×
    FrontC                             0.004s     0.004s      3.17MB      2×
    Cabs2cil                           0.006s     0.006s      3.36MB      2×
    global_inits                       0.001s     0.001s      0.18MB      1×
    solving                           11.487s    11.487s    283.09MB      1×
      S.Dom.equal                        0.001s     0.001s      0.04MB    117×
      base unassume                      0.242s     0.242s    191.91MB     11×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.057s     0.057s     16.43MB      1×
        postsolver_iter                    0.057s     0.057s     16.38MB      1×
    warn_global                        0.001s     0.001s      0.17MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
