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


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Error][Witness] CIL couldn't parse invariant: cond == (1) (../plain/lcm2_valuebound20.c:16:5)
[Info][Witness] invariant has undefined variables or side effects: cond == (1) (../plain/lcm2_valuebound20.c:16:5)
../plain/lcm2_valuebound20.c:16: Error: Cannot resolve variable cond.
[Warning][Witness] couldn't locate invariant: (a >= (0U) && a <= (20U) && x == y) || (a <= (20U) && !(x == y) && a >= (0U) && !((4294967295U) == y) && !(y == (4294967295U))) || (a <= (20U) && !(x == y) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && a >= (0U) && !(x >= (0U))) || (a <= (20U) && !(x == y) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && a >= (0U) && x >= (0U) && !(x <= (4294967295U))) || (a <= (20U) && !(x == y) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && x <= (4294967295U) && a >= (0U) && b >= (0U) && b <= (20U) && u == b && v == a && x >= (0U) && x <= (20U) && y == b) || (a <= (20U) && !(x == y) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && x <= (4294967295U) && (!(b >= (0U)) || (b >= (0U) && !(b <= (20U))) || (b >= (0U) && b <= (20U) && !(u == b)) || (b >= (0U) && b <= (20U) && u == b && !(y == b))) && a >= (0U) && u == (((b + v) + v) + v) && v == a && x >= (0U) && x <= (20U) && y == x) || (a <= (20U) && !(x == y) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && x >= (0U) && x <= (4294967295U) && (!(b >= (0U)) || (b >= (0U) && !(b <= (20U))) || (b >= (0U) && b <= (20U) && !(u == b)) || (b >= (0U) && b <= (20U) && u == b && !(v == a)) || (b >= (0U) && b <= (20U) && u == b && v == a && !(x <= (20U))) || (b >= (0U) && b <= (20U) && u == b && v == a && x <= (20U) && !(y == b))) && (!(u == (((b + v) + v) + v)) || (u == (((b + v) + v) + v) && !(v == a)) || (u == (((b + v) + v) + v) && v == a && !(x <= (20U))) || (u == (((b + v) + v) + v) && v == a && x <= (20U) && !(y == x))) && a >= (0U) && !(y >= (0U))) || (a <= (20U) && !(x == y) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && x >= (0U) && x <= (4294967295U) && (!(b >= (0U)) || (b >= (0U) && !(b <= (20U))) || (b >= (0U) && b <= (20U) && !(u == b)) || (b >= (0U) && b <= (20U) && u == b && !(v == a)) || (b >= (0U) && b <= (20U) && u == b && v == a && !(x <= (20U))) || (b >= (0U) && b <= (20U) && u == b && v == a && x <= (20U) && !(y == b))) && (!(u == (((b + v) + v) + v)) || (u == (((b + v) + v) + v) && !(v == a)) || (u == (((b + v) + v) + v) && v == a && !(x <= (20U))) || (u == (((b + v) + v) + v) && v == a && x <= (20U) && !(y == x))) && a >= (0U) && y >= (0U) && !(y <= (4294967295U))) || (a <= (20U) && !(a >= (0U)) && a >= (1U) && b >= (0U) && b <= (19U) && u == b && v == ((a + u) + u) && x == y && y >= (0U) && y <= (19U)) (../plain/lcm2_valuebound20.c:41:13)
[Info][Witness] unassume invariant: (((((((((((a <= 20U && a >= 1U) && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 19U) || (((a <= 20U && ((((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y >= 0U))) || ((((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && ! (y <= 19U)))) && a >= 0U) && ! (y == 4294967295U))) || ((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u))) && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && a >= 0U)) && (((((((((((a <= 20U && a >= 1U) && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 19U) || (((a <= 20U && ((((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y >= 0U))) || ((((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && ! (y <= 19U)))) && a >= 0U) && ! (y == 4294967295U))) || ((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u))) && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && a >= 0U)) (../plain/lcm2_valuebound20.c:35:5-35:10)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound20.c:38:9-38:46)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/lcm2_valuebound20.c:47:13-47:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound20.c:48:13-48:22)
[Info][Witness] unassume invariant: (((((((((((a <= 20U && a >= 1U) && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 19U) || (((a <= 20U && ((((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y >= 0U))) || ((((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && ! (y <= 19U)))) && a >= 0U) && ! (y == 4294967295U))) || ((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u))) && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && a >= 0U)) && (((((((((((a <= 20U && a >= 1U) && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 19U) || (((a <= 20U && ((((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y >= 0U))) || ((((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && ! (y <= 19U)))) && a >= 0U) && ! (y == 4294967295U))) || ((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u))) && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && a >= 0U)) (../plain/lcm2_valuebound20.c:48:13-48:22)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/lcm2_valuebound20.c:44:13-44:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound20.c:45:13-45:22)
[Info][Witness] unassume invariant: (((((((((((a <= 20U && a >= 1U) && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 19U) || (((a <= 20U && ((((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y >= 0U))) || ((((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && ! (y <= 19U)))) && a >= 0U) && ! (y == 4294967295U))) || ((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u))) && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && a >= 0U)) && (((((((((((a <= 20U && a >= 1U) && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 19U) || (((a <= 20U && ((((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y >= 0U))) || ((((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && ! (y <= 19U)))) && a >= 0U) && ! (y == 4294967295U))) || ((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u))) && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((a <= 20U && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 19U))) || (((a >= 1U && b >= 0U) && b <= 19U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 19U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 19U)))) && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && a >= 0U)) (../plain/lcm2_valuebound20.c:45:13-45:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound20.c:52:5-52:42)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 32
  dead: 0
  total lines: 32
[Warning][Deadcode][CWE-571] condition 'b >= 0U' (possibly inserted by CIL) is always true (../plain/lcm2_valuebound20.c:25:5-25:39)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/lcm2_valuebound20.c:37:12-37:13)
[Warning][Deadcode][CWE-571] condition 'a >= 0U' (possibly inserted by CIL) is always true (../plain/lcm2_valuebound20.c:23:5-23:39)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow
[Warning][Witness] invariant unconfirmed: (a <= (20U) && a >= (1U) && b >= (0U) && b <= (19U) && u == b && v == (((a + u) + u) + u) && y >= (0U) && y <= (19U)) || (a <= (20U) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (19U))) || (a >= (1U) && b >= (0U) && b <= (19U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (19U) && u == b && !(v == (((a + u) + u) + u))) || (a >= (1U) && b >= (0U) && b <= (19U) && u == b && v == (((a + u) + u) + u) && !(y >= (0U))) || (a >= (1U) && b >= (0U) && b <= (19U) && u == b && v == (((a + u) + u) + u) && y >= (0U) && !(y <= (19U)))) && a >= (0U) && !(y == (4294967295U))) || (a <= (20U) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (19U))) || (a >= (1U) && b >= (0U) && b <= (19U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (19U) && u == b && !(v == (((a + u) + u) + u))) || (a >= (1U) && b >= (0U) && b <= (19U) && u == b && v == (((a + u) + u) + u))) && y == (4294967295U) && a >= (0U) && !(y >= (0U))) || (a <= (20U) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (19U))) || (a >= (1U) && b >= (0U) && b <= (19U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (19U) && u == b && !(v == (((a + u) + u) + u))) || (a >= (1U) && b >= (0U) && b <= (19U) && u == b && v == (((a + u) + u) + u) && !(y <= (19U)))) && y == (4294967295U) && a >= (0U) && y >= (0U) && !(y <= (4294967295U))) || (a <= (20U) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (19U))) || (a >= (1U) && b >= (0U) && b <= (19U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (19U) && u == b && !(v == (((a + u) + u) + u))) || (a >= (1U) && b >= (0U) && b <= (19U) && u == b && v == (((a + u) + u) + u) && !(y <= (19U)))) && y == (4294967295U) && y >= (0U) && y <= (4294967295U) && a >= (0U)) (../plain/lcm2_valuebound20.c:37:5)
../plain/lcm2_valuebound20.c:16: Error: Cannot resolve variable cond.
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 2
  refuted: 0
  error: 2
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 4
SV-COMP result: unknown

vars = 75    evals = 128    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            3.988s     3.989s    240.02MB      1×
  preprocess                         0.025s     0.024s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.13MB      4×
  Cabs2cil                           0.006s     0.006s      4.78MB      4×
  mergeCIL                           0.005s     0.005s      3.34MB      1×
  analysis                           3.944s     3.945s    222.76MB      1×
    createCFG                          0.001s     0.001s      0.67MB      1×
      handle                             0.001s     0.001s      0.11MB     34×
      iter_connect                       0.001s     0.001s      0.45MB     34×
        computeSCCs                        0.001s     0.001s      0.27MB     35×
    FrontC                             0.002s     0.002s      1.61MB      6×
    Cabs2cil                           0.003s     0.003s      2.01MB      6×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            3.594s     3.594s    196.76MB      1×
      S.Dom.equal                        0.001s     0.001s      0.05MB    130×
      base unassume                      0.188s     0.188s    127.64MB     16×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.109s     0.109s     17.54MB      1×
        postsolver_iter                    0.109s     0.109s     17.47MB      1×
    warn_global                        0.001s     0.001s      0.21MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
