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

|rho|=42
|called|=4
|stable|=30
|infl|=38
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=30
Found 2 contexts for 2 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/sumt6.c:16:1-39:1

Memory statistics: total=492.60MB, max=24.88MB, minor=489.71MB, major=55.54MB, promoted=52.64MB
    minor collections=255  major collections=11 compactions=0

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

Timings:
                                  cputime   walltime   allocated   count
Default                           18.110s    18.132s    759.12MB      1×
  preprocess                         0.025s     0.024s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.13MB      4×
  Cabs2cil                           0.006s     0.006s      4.76MB      4×
  mergeCIL                           0.004s     0.004s      3.35MB      1×
  analysis                          18.066s    18.087s    741.89MB      1×
    createCFG                          0.001s     0.001s      0.65MB      1×
      handle                             0.001s     0.001s      0.10MB     34×
      iter_connect                       0.001s     0.001s      0.43MB     34×
        computeSCCs                        0.001s     0.001s      0.25MB     35×
    FrontC                             0.009s     0.009s      5.17MB      2×
    Cabs2cil                           0.004s     0.004s      4.50MB      2×
    global_inits                       0.001s     0.001s      0.18MB      1×
    solving                           11.249s    11.251s    525.53MB      1×
      S.Dom.equal                        0.001s     0.001s      0.04MB    104×
      base unassume                      0.531s     0.531s    407.01MB     11×
      cheap_full_reach                   0.001s     0.001s      0.02MB      1×
      postsolver                         0.032s     0.032s     16.17MB      1×
        postsolver_iter                    0.032s     0.032s     16.12MB      1×
    warn_global                        0.001s     0.001s      0.15MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
