/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_valuebound5.yml.witness.yml --witness.yaml.validate pesco/lcm2_valuebound5.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/lcm2_valuebound5.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_valuebound5.c:16:5)
[Info][Witness] invariant has undefined variables or side effects: cond == (1) (../plain/lcm2_valuebound5.c:16:5)
[Warning][Witness] couldn't locate invariant: (a <= (5U) && a >= (0U) && !((4294967295U) == y) && !(y == (4294967295U))) || (a <= (5U) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && a >= (0U) && !(x >= (0U))) || (a <= (5U) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && a >= (0U) && x >= (0U) && !(x <= (4294967295U))) || (a <= (5U) && (!(a >= (0U)) || (a >= (0U) && (4294967295U) == y) || (a >= (0U) && !((4294967295U) == y) && y == (4294967295U))) && (!(a >= (0U)) || (a >= (0U) && x >= (0U) && x <= (4294967295U))) && a >= (1U) && b >= (0U) && b <= (4U) && u == b && v == ((a + u) + u) && x == y && y >= (0U) && y <= (4U)) || (a <= (5U) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && x <= (4294967295U) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (4U))) || (a >= (1U) && b >= (0U) && b <= (4U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && !(v == ((a + u) + u))) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && v == ((a + u) + u) && !(x == y)) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && v == ((a + u) + u) && x == y && !(y >= (0U))) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && v == ((a + u) + u) && x == y && y >= (0U) && !(y <= (4U)))) && a >= (0U) && u == (((b + v) + v) + v) && v == a && x >= (0U) && x <= (5U) && y == x) || (a <= (5U) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && x <= (4294967295U) && (!(a >= (1U)) || (a >= (1U) && !(b <= (4U))) || (a >= (1U) && b <= (4U) && !(v == ((a + u) + u))) || (a >= (1U) && b <= (4U) && v == ((a + u) + u) && !(x == y)) || (a >= (1U) && b <= (4U) && v == ((a + u) + u) && x == y && !(y >= (0U))) || (a >= (1U) && b <= (4U) && v == ((a + u) + u) && x == y && y >= (0U) && !(y <= (4U)))) && (!(u == (((b + v) + v) + v)) || (u == (((b + v) + v) + v) && !(y == x))) && a >= (0U) && b >= (0U) && b <= (5U) && u == b && v == a && x >= (0U) && x <= (5U) && y == b) || (a <= (5U) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && x >= (0U) && x <= (4294967295U) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (4U))) || (a >= (1U) && b >= (0U) && b <= (4U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && !(v == ((a + u) + u))) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && v == ((a + u) + u) && !(x == y)) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && v == ((a + u) + u) && x == y)) && (!(u == (((b + v) + v) + v)) || (u == (((b + v) + v) + v) && !(v == a)) || (u == (((b + v) + v) + v) && v == a && !(x <= (5U))) || (u == (((b + v) + v) + v) && v == a && x <= (5U) && !(y == x))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (5U))) || (b >= (0U) && b <= (5U) && !(u == b)) || (b >= (0U) && b <= (5U) && u == b && !(v == a)) || (b >= (0U) && b <= (5U) && u == b && v == a && !(x <= (5U))) || (b >= (0U) && b <= (5U) && u == b && v == a && x <= (5U) && !(y == b))) && a >= (0U) && !(y >= (0U))) || (a <= (5U) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && x >= (0U) && x <= (4294967295U) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (4U))) || (a >= (1U) && b >= (0U) && b <= (4U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && !(v == ((a + u) + u))) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && v == ((a + u) + u) && !(x == y)) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && v == ((a + u) + u) && x == y && !(y <= (4U)))) && (!(u == (((b + v) + v) + v)) || (u == (((b + v) + v) + v) && !(v == a)) || (u == (((b + v) + v) + v) && v == a && !(x <= (5U))) || (u == (((b + v) + v) + v) && v == a && x <= (5U) && !(y == x))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (5U))) || (b >= (0U) && b <= (5U) && !(u == b)) || (b >= (0U) && b <= (5U) && u == b && !(v == a)) || (b >= (0U) && b <= (5U) && u == b && v == a && !(x <= (5U))) || (b >= (0U) && b <= (5U) && u == b && v == a && x <= (5U) && !(y == b))) && a >= (0U) && y >= (0U) && !(y <= (4294967295U))) || (a <= (5U) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && x >= (0U) && x <= (4294967295U) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (4U))) || (a >= (1U) && b >= (0U) && b <= (4U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && !(v == ((a + u) + u))) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && v == ((a + u) + u) && !(y <= (4U)))) && (!(u == (((b + v) + v) + v)) || (u == (((b + v) + v) + v) && !(v == a)) || (u == (((b + v) + v) + v) && v == a && !(x <= (5U))) || (u == (((b + v) + v) + v) && v == a && x <= (5U) && !(y == x))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (5U))) || (b >= (0U) && b <= (5U) && !(u == b)) || (b >= (0U) && b <= (5U) && u == b && !(v == a)) || (b >= (0U) && b <= (5U) && u == b && v == a && !(x <= (5U))) || (b >= (0U) && b <= (5U) && u == b && v == a && x <= (5U) && !(y == b))) && y >= (0U) && y <= (4294967295U) && a >= (0U) && x == y) (../plain/lcm2_valuebound5.c:41:13)
../plain/lcm2_valuebound5.c:16: Error: Cannot resolve variable cond.
[Info][Witness] unassume invariant: ((((((a <= 5U && a >= 0U) && ! (y >= 0U)) || (((a <= 5U && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || ((((a <= 5U && y >= 0U) && y <= 4294967295U) && a >= 0U) && ! (y == 4294967295U))) || (((((((((a <= 5U && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && a >= 1U) && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 4U)) || (((((a <= 5U && y >= 0U) && y <= 4294967295U) && y == 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 4U))) || (((a >= 1U && b >= 0U) && b <= 4U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 4U)))) && a >= 0U)) && ((((((a <= 5U && a >= 0U) && ! (y >= 0U)) || (((a <= 5U && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || ((((a <= 5U && y >= 0U) && y <= 4294967295U) && a >= 0U) && ! (y == 4294967295U))) || (((((((((a <= 5U && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && a >= 1U) && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 4U)) || (((((a <= 5U && y >= 0U) && y <= 4294967295U) && y == 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 4U))) || (((a >= 1U && b >= 0U) && b <= 4U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 4U)))) && a >= 0U)) (../plain/lcm2_valuebound5.c:35:5-35:10)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound5.c:38:9-38:46)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/lcm2_valuebound5.c:47:13-47:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound5.c:48:13-48:22)
[Info][Witness] unassume invariant: ((((((a <= 5U && a >= 0U) && ! (y >= 0U)) || (((a <= 5U && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || ((((a <= 5U && y >= 0U) && y <= 4294967295U) && a >= 0U) && ! (y == 4294967295U))) || (((((((((a <= 5U && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && a >= 1U) && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 4U)) || (((((a <= 5U && y >= 0U) && y <= 4294967295U) && y == 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 4U))) || (((a >= 1U && b >= 0U) && b <= 4U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 4U)))) && a >= 0U)) && ((((((a <= 5U && a >= 0U) && ! (y >= 0U)) || (((a <= 5U && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || ((((a <= 5U && y >= 0U) && y <= 4294967295U) && a >= 0U) && ! (y == 4294967295U))) || (((((((((a <= 5U && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && a >= 1U) && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 4U)) || (((((a <= 5U && y >= 0U) && y <= 4294967295U) && y == 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 4U))) || (((a >= 1U && b >= 0U) && b <= 4U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 4U)))) && a >= 0U)) (../plain/lcm2_valuebound5.c:48:13-48:22)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/lcm2_valuebound5.c:44:13-44:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound5.c:45:13-45:22)
[Info][Witness] unassume invariant: ((((((a <= 5U && a >= 0U) && ! (y >= 0U)) || (((a <= 5U && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || ((((a <= 5U && y >= 0U) && y <= 4294967295U) && a >= 0U) && ! (y == 4294967295U))) || (((((((((a <= 5U && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && a >= 1U) && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 4U)) || (((((a <= 5U && y >= 0U) && y <= 4294967295U) && y == 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 4U))) || (((a >= 1U && b >= 0U) && b <= 4U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 4U)))) && a >= 0U)) && ((((((a <= 5U && a >= 0U) && ! (y >= 0U)) || (((a <= 5U && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || ((((a <= 5U && y >= 0U) && y <= 4294967295U) && a >= 0U) && ! (y == 4294967295U))) || (((((((((a <= 5U && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && a >= 1U) && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 4U)) || (((((a <= 5U && y >= 0U) && y <= 4294967295U) && y == 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 4U))) || (((a >= 1U && b >= 0U) && b <= 4U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 4U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 4U)))) && a >= 0U)) (../plain/lcm2_valuebound5.c:45:13-45:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound5.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_valuebound5.c:25:5-25:38)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/lcm2_valuebound5.c:37:12-37:13)
[Warning][Deadcode][CWE-571] condition 'a >= 0U' (possibly inserted by CIL) is always true (../plain/lcm2_valuebound5.c:23:5-23:38)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow
[Warning][Witness] invariant unconfirmed: (a <= (5U) && a >= (0U) && !(y >= (0U))) || (a <= (5U) && a >= (0U) && y >= (0U) && !(y <= (4294967295U))) || (a <= (5U) && y >= (0U) && y <= (4294967295U) && a >= (0U) && !(y == (4294967295U))) || (a <= (5U) && (!(a >= (0U)) || (a >= (0U) && y <= (4294967295U))) && (!(a >= (0U)) || (a >= (0U) && y == (4294967295U))) && a >= (1U) && b >= (0U) && b <= (4U) && u == b && v == (((a + u) + u) + u) && y >= (0U) && y <= (4U)) || (a <= (5U) && y >= (0U) && y <= (4294967295U) && y == (4294967295U) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (4U))) || (a >= (1U) && b >= (0U) && b <= (4U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && !(v == (((a + u) + u) + u))) || (a >= (1U) && b >= (0U) && b <= (4U) && u == b && v == (((a + u) + u) + u) && !(y <= (4U)))) && a >= (0U)) (../plain/lcm2_valuebound5.c:37:5)
../plain/lcm2_valuebound5.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                            1.692s     1.697s    153.70MB      1×
  preprocess                         0.024s     0.023s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.13MB      4×
  Cabs2cil                           0.005s     0.005s      4.78MB      4×
  mergeCIL                           0.003s     0.003s      3.34MB      1×
  analysis                           1.651s     1.656s    136.43MB      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.008s     0.008s      0.72MB      6×
    Cabs2cil                           0.005s     0.005s      1.19MB      6×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            1.525s     1.526s    118.52MB      1×
      S.Dom.equal                        0.001s     0.001s      0.05MB    130×
      base unassume                      0.085s     0.085s     57.49MB     16×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.102s     0.102s     16.65MB      1×
        postsolver_iter                    0.102s     0.102s     16.58MB      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×
