/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 pesco/knuth_unwindbound2.yml.witness.yml --witness.yaml.validate pesco/knuth_unwindbound2.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/knuth_unwindbound2.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Witness] couldn't locate invariant: (counter == (2) && d == (a + (2U)) && k == t && t >= (1U) && t <= (4294967294U)) || ((!(counter == (2)) || (counter == (2) && !(d == (a + (2U)))) || (counter == (2) && d == (a + (2U)) && !(k == t)) || (counter == (2) && d == (a + (2U)) && k == t && !(t >= (1U))) || (counter == (2) && d == (a + (2U)) && k == t && t >= (1U) && !(t <= (4294967294U)))) && counter == (1) && d == a && !(k == (4294967295U)) && !(r == (4294967295U)) && t == (0U)) (../plain/knuth_unwindbound2.i:41:9)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:37:5-37:20)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:38:5-38:34)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:38:5-38:34)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (../plain/knuth_unwindbound2.i:39:5-39:16)
[Info][Witness] unassume invariant: ((((((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && t <= 4294967294U) || (((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && counter == 0) && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && t == 0U)) || (((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && counter == 2) && d == a + 4U) && ! (0U == t)) && ! (t == 0U))) || (((((((! (counter == 1) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || ((((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && ! (t == 0U)))) && ((! (d == a + 4U) || (d == a + 4U && 0U == t)) || ((d == a + 4U && ! (0U == t)) && t == 0U))) && counter == 2) && d == a + 2U) && k == t) && t >= 1U) && t <= 4294967294U)) || (((((((((((! (d == a + 2U) || (d == a + 2U && ! (k == t))) || ((d == a + 2U && k == t) && ! (t >= 1U))) || (((d == a + 2U && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ! (counter == 0)) && (((! (counter == 2) || (counter == 2 && ! (d == a + 4U))) || ((counter == 2 && d == a + 4U) && 0U == t)) || ((counter == 2 && d == a + 4U) && ! (0U == t)))) && ((((! (counter == 2) || (counter == 2 && ! (d == a + 2U))) || ((counter == 2 && d == a + 2U) && ! (k == t))) || (((counter == 2 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 2 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U)))) && counter == 1) && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && t == 0U)) || (((((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && ! (counter == 2)) && ((((! (counter == 1) || (counter == 1 && ! (d == a))) || ((counter == 1 && d == a) && k == 4294967295U)) || (((counter == 1 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 1 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && counter == 3) && d == a + 4U) && ! (0U == t)) && ! (t == 0U)) (../plain/knuth_unwindbound2.i:39:5-39:16)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:41:9-41:90)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:41:9-41:90)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:42:9-42:42)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:43:9-43:118)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:43:9-43:118)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:44:9-44:62)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:44:9-44:62)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:46:13-46:26)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:46:13-46:26)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:52:21-52:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:52:21-52:63)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:52:21-52:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:52:21-52:63)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:57:21-57:95)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:57:21-57:95)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:57:21-57:95)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:57:21-57:95)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:57:21-57:95)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:57:21-57:95)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:65:13-65:42)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:65:13-65:42)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:67:13-67:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:68:13-68:22)
[Info][Witness] unassume invariant: ((((((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && t <= 4294967294U) || (((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && counter == 0) && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && t == 0U)) || (((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && counter == 2) && d == a + 4U) && ! (0U == t)) && ! (t == 0U))) || (((((((! (counter == 1) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || ((((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && ! (t == 0U)))) && ((! (d == a + 4U) || (d == a + 4U && 0U == t)) || ((d == a + 4U && ! (0U == t)) && t == 0U))) && counter == 2) && d == a + 2U) && k == t) && t >= 1U) && t <= 4294967294U)) || (((((((((((! (d == a + 2U) || (d == a + 2U && ! (k == t))) || ((d == a + 2U && k == t) && ! (t >= 1U))) || (((d == a + 2U && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ! (counter == 0)) && (((! (counter == 2) || (counter == 2 && ! (d == a + 4U))) || ((counter == 2 && d == a + 4U) && 0U == t)) || ((counter == 2 && d == a + 4U) && ! (0U == t)))) && ((((! (counter == 2) || (counter == 2 && ! (d == a + 2U))) || ((counter == 2 && d == a + 2U) && ! (k == t))) || (((counter == 2 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 2 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U)))) && counter == 1) && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && t == 0U)) || (((((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && ! (counter == 2)) && ((((! (counter == 1) || (counter == 1 && ! (d == a))) || ((counter == 1 && d == a) && k == 4294967295U)) || (((counter == 1 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 1 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && counter == 3) && d == a + 4U) && ! (0U == t)) && ! (t == 0U)) (../plain/knuth_unwindbound2.i:68:13-68:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:59:13-59:38)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:59:13-59:38)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:61:13-61:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:62:13-62:22)
[Info][Witness] unassume invariant: ((((((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && t <= 4294967294U) || (((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && counter == 0) && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && t == 0U)) || (((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && counter == 2) && d == a + 4U) && ! (0U == t)) && ! (t == 0U))) || (((((((! (counter == 1) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || ((((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && ! (t == 0U)))) && ((! (d == a + 4U) || (d == a + 4U && 0U == t)) || ((d == a + 4U && ! (0U == t)) && t == 0U))) && counter == 2) && d == a + 2U) && k == t) && t >= 1U) && t <= 4294967294U)) || (((((((((((! (d == a + 2U) || (d == a + 2U && ! (k == t))) || ((d == a + 2U && k == t) && ! (t >= 1U))) || (((d == a + 2U && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ! (counter == 0)) && (((! (counter == 2) || (counter == 2 && ! (d == a + 4U))) || ((counter == 2 && d == a + 4U) && 0U == t)) || ((counter == 2 && d == a + 4U) && ! (0U == t)))) && ((((! (counter == 2) || (counter == 2 && ! (d == a + 2U))) || ((counter == 2 && d == a + 2U) && ! (k == t))) || (((counter == 2 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 2 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U)))) && counter == 1) && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && t == 0U)) || (((((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && ! (counter == 2)) && ((((! (counter == 1) || (counter == 1 && ! (d == a))) || ((counter == 1 && d == a) && k == 4294967295U)) || (((counter == 1 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 1 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && counter == 3) && d == a + 4U) && ! (0U == t)) && ! (t == 0U)) (../plain/knuth_unwindbound2.i:62:13-62:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:54:13-54:30)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:54:13-54:30)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:56:13-56:22)
[Info][Witness] unassume invariant: ((((((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && t <= 4294967294U) || (((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && counter == 0) && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && t == 0U)) || (((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && counter == 2) && d == a + 4U) && ! (0U == t)) && ! (t == 0U))) || (((((((! (counter == 1) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || ((((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && ! (t == 0U)))) && ((! (d == a + 4U) || (d == a + 4U && 0U == t)) || ((d == a + 4U && ! (0U == t)) && t == 0U))) && counter == 2) && d == a + 2U) && k == t) && t >= 1U) && t <= 4294967294U)) || (((((((((((! (d == a + 2U) || (d == a + 2U && ! (k == t))) || ((d == a + 2U && k == t) && ! (t >= 1U))) || (((d == a + 2U && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ! (counter == 0)) && (((! (counter == 2) || (counter == 2 && ! (d == a + 4U))) || ((counter == 2 && d == a + 4U) && 0U == t)) || ((counter == 2 && d == a + 4U) && ! (0U == t)))) && ((((! (counter == 2) || (counter == 2 && ! (d == a + 2U))) || ((counter == 2 && d == a + 2U) && ! (k == t))) || (((counter == 2 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 2 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U)))) && counter == 1) && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && t == 0U)) || (((((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && ! (counter == 2)) && ((((! (counter == 1) || (counter == 1 && ! (d == a))) || ((counter == 1 && d == a) && k == 4294967295U)) || (((counter == 1 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 1 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && counter == 3) && d == a + 4U) && ! (0U == t)) && ! (t == 0U)) (../plain/knuth_unwindbound2.i:56:13-56:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:48:13-48:38)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/knuth_unwindbound2.i:48:13-48:38)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:50:13-50:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/knuth_unwindbound2.i:51:13-51:22)
[Info][Witness] unassume invariant: ((((((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && t <= 4294967294U) || (((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && counter == 0) && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && t == 0U)) || (((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && counter == 2) && d == a + 4U) && ! (0U == t)) && ! (t == 0U))) || (((((((! (counter == 1) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || ((((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && ! (t == 0U)))) && ((! (d == a + 4U) || (d == a + 4U && 0U == t)) || ((d == a + 4U && ! (0U == t)) && t == 0U))) && counter == 2) && d == a + 2U) && k == t) && t >= 1U) && t <= 4294967294U)) || (((((((((((! (d == a + 2U) || (d == a + 2U && ! (k == t))) || ((d == a + 2U && k == t) && ! (t >= 1U))) || (((d == a + 2U && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ! (counter == 0)) && (((! (counter == 2) || (counter == 2 && ! (d == a + 4U))) || ((counter == 2 && d == a + 4U) && 0U == t)) || ((counter == 2 && d == a + 4U) && ! (0U == t)))) && ((((! (counter == 2) || (counter == 2 && ! (d == a + 2U))) || ((counter == 2 && d == a + 2U) && ! (k == t))) || (((counter == 2 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 2 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U)))) && counter == 1) && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)) && t == 0U)) || (((((((((((! (counter == 1) || (counter == 1 && ! (d == a + 2U))) || ((counter == 1 && d == a + 2U) && ! (k == t))) || (((counter == 1 && d == a + 2U) && k == t) && ! (t >= 1U))) || ((((counter == 1 && d == a + 2U) && k == t) && t >= 1U) && ! (t <= 4294967294U))) && ((((! (counter == 0) || (counter == 0 && ! (d == a))) || ((counter == 0 && d == a) && k == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 0 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && ! (counter == 2)) && ((((! (counter == 1) || (counter == 1 && ! (d == a))) || ((counter == 1 && d == a) && k == 4294967295U)) || (((counter == 1 && d == a) && ! (k == 4294967295U)) && r == 4294967295U)) || (((counter == 1 && d == a) && ! (k == 4294967295U)) && ! (r == 4294967295U)))) && counter == 3) && d == a + 4U) && ! (0U == t)) && ! (t == 0U)) (../plain/knuth_unwindbound2.i:51:13-51:22)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 49
  dead: 0
  total lines: 49
[Warning][Deadcode][CWE-571] condition '2U * r + q >= k' is always true (../plain/knuth_unwindbound2.i:52:21-52:63)
[Warning][Deadcode][CWE-571] condition '2U * r + q >= k' is always true (../plain/knuth_unwindbound2.i:57:21-57:95)
[Warning][Deadcode][CWE-571] condition '2U * r + q >= (d + k) + 2U' is always true (../plain/knuth_unwindbound2.i:57:21-57:95)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (../plain/knuth_unwindbound2.i:12:73-12:74)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow
[Warning][Witness] invariant unconfirmed: (counter == (1) && d == (a + (2U)) && k == t && t >= (1U) && t <= (4294967294U)) || ((!(counter == (1)) || (counter == (1) && !(d == (a + (2U)))) || (counter == (1) && d == (a + (2U)) && !(k == t)) || (counter == (1) && d == (a + (2U)) && k == t && !(t >= (1U))) || (counter == (1) && d == (a + (2U)) && k == t && t >= (1U) && !(t <= (4294967294U)))) && counter == (0) && d == a && !(k == (4294967295U)) && !(r == (4294967295U)) && t == (0U)) || ((!(counter == (1)) || (counter == (1) && !(d == (a + (2U)))) || (counter == (1) && d == (a + (2U)) && !(k == t)) || (counter == (1) && d == (a + (2U)) && k == t && !(t >= (1U))) || (counter == (1) && d == (a + (2U)) && k == t && t >= (1U) && !(t <= (4294967294U)))) && (!(counter == (0)) || (counter == (0) && !(d == a)) || (counter == (0) && d == a && k == (4294967295U)) || (counter == (0) && d == a && !(k == (4294967295U)) && r == (4294967295U)) || (counter == (0) && d == a && !(k == (4294967295U)) && !(r == (4294967295U)))) && counter == (2) && d == (a + (4U)) && !((0U) == t) && !(t == (0U))) || (!(counter == (1)) && (!(counter == (0)) || (counter == (0) && !(d == a)) || (counter == (0) && d == a && k == (4294967295U)) || (counter == (0) && d == a && !(k == (4294967295U)) && r == (4294967295U)) || (counter == (0) && d == a && !(k == (4294967295U)) && !(r == (4294967295U)) && !(t == (0U)))) && (!(d == (a + (4U))) || (d == (a + (4U)) && (0U) == t) || (d == (a + (4U)) && !((0U) == t) && t == (0U))) && counter == (2) && d == (a + (2U)) && k == t && t >= (1U) && t <= (4294967294U)) || ((!(d == (a + (2U))) || (d == (a + (2U)) && !(k == t)) || (d == (a + (2U)) && k == t && !(t >= (1U))) || (d == (a + (2U)) && k == t && t >= (1U) && !(t <= (4294967294U)))) && !(counter == (0)) && (!(counter == (2)) || (counter == (2) && !(d == (a + (4U)))) || (counter == (2) && d == (a + (4U)) && (0U) == t) || (counter == (2) && d == (a + (4U)) && !((0U) == t))) && (!(counter == (2)) || (counter == (2) && !(d == (a + (2U)))) || (counter == (2) && d == (a + (2U)) && !(k == t)) || (counter == (2) && d == (a + (2U)) && k == t && !(t >= (1U))) || (counter == (2) && d == (a + (2U)) && k == t && t >= (1U) && !(t <= (4294967294U)))) && counter == (1) && d == a && !(k == (4294967295U)) && !(r == (4294967295U)) && t == (0U)) || ((!(counter == (1)) || (counter == (1) && !(d == (a + (2U)))) || (counter == (1) && d == (a + (2U)) && !(k == t)) || (counter == (1) && d == (a + (2U)) && k == t && !(t >= (1U))) || (counter == (1) && d == (a + (2U)) && k == t && t >= (1U) && !(t <= (4294967294U)))) && (!(counter == (0)) || (counter == (0) && !(d == a)) || (counter == (0) && d == a && k == (4294967295U)) || (counter == (0) && d == a && !(k == (4294967295U)) && r == (4294967295U)) || (counter == (0) && d == a && !(k == (4294967295U)) && !(r == (4294967295U)))) && !(counter == (2)) && (!(counter == (1)) || (counter == (1) && !(d == a)) || (counter == (1) && d == a && k == (4294967295U)) || (counter == (1) && d == a && !(k == (4294967295U)) && r == (4294967295U)) || (counter == (1) && d == a && !(k == (4294967295U)) && !(r == (4294967295U)))) && counter == (3) && d == (a + (4U)) && !((0U) == t) && !(t == (0U))) (../plain/knuth_unwindbound2.i:40:5)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 1
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 2
SV-COMP result: unknown

vars = 104    evals = 305    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                            3.280s     3.280s    327.25MB      1×
  preprocess                         0.026s     0.025s      0.01MB      1×
  FrontC                             0.006s     0.006s      4.33MB      4×
  Cabs2cil                           0.006s     0.006s      5.11MB      4×
  mergeCIL                           0.004s     0.004s      3.38MB      1×
  analysis                           3.234s     3.235s    309.38MB      1×
    createCFG                          0.001s     0.001s      0.70MB      1×
      handle                             0.001s     0.001s      0.13MB     34×
      iter_connect                       0.001s     0.001s      0.45MB     34×
        computeSCCs                        0.001s     0.001s      0.27MB     35×
    FrontC                             0.002s     0.002s      1.22MB      2×
    Cabs2cil                           0.002s     0.002s      1.21MB      2×
    global_inits                       0.001s     0.001s      0.18MB      1×
    solving                            2.678s     2.678s    283.92MB      1×
      S.Dom.equal                        0.001s     0.002s      0.11MB    306×
      base unassume                      0.137s     0.137s    131.28MB     21×
      cheap_full_reach                   0.001s     0.001s      0.04MB      1×
      postsolver                         0.107s     0.107s     27.71MB      1×
        postsolver_iter                    0.106s     0.106s     27.63MB      1×
    warn_global                        0.001s     0.001s      0.30MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
