/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_valuebound100.yml.witness.yml --witness.yaml.validate pesco/lcm2_valuebound100.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/lcm2_valuebound100.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_valuebound100.c:16:5)
[Info][Witness] invariant has undefined variables or side effects: cond == (1) (../plain/lcm2_valuebound100.c:16:5)
[Warning][Witness] couldn't locate invariant: (a <= (100U) && a >= (0U) && !(y >= (0U))) || (a <= (100U) && a >= (0U) && y >= (0U) && !(y <= (4294967295U))) || (a <= (100U) && y >= (0U) && y <= (4294967295U) && a >= (0U) && x == y) || (a <= (100U) && y >= (0U) && y <= (4294967295U) && !(x == y) && a >= (0U) && !((4294967295U) == y) && !(y == (4294967295U))) || (a <= (100U) && !(a >= (0U)) && a >= (1U) && b >= (0U) && b <= (99U) && u == b && v == ((a + u) + u) && x == y && y >= (0U) && y <= (99U)) || (a <= (100U) && y >= (0U) && y <= (4294967295U) && !(x == y) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (99U))) || (a >= (1U) && b >= (0U) && b <= (99U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (99U) && u == b && !(v == ((a + u) + u))) || (a >= (1U) && b >= (0U) && b <= (99U) && u == b && v == ((a + u) + u))) && a >= (0U) && u == (((b + v) + v) + v) && v == a && x >= (0U) && x <= (100U) && y == x) || (a <= (100U) && y >= (0U) && y <= (4294967295U) && !(x == y) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && (!(a >= (1U)) || (a >= (1U) && !(b <= (99U))) || (a >= (1U) && b <= (99U) && !(v == ((a + u) + u))) || (a >= (1U) && b <= (99U) && v == ((a + u) + u))) && (!(u == (((b + v) + v) + v)) || (u == (((b + v) + v) + v) && !(y == x))) && a >= (0U) && b >= (0U) && b <= (100U) && u == b && v == a && x >= (0U) && x <= (100U) && y == b) || (a <= (100U) && y >= (0U) && y <= (4294967295U) && !(x == y) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (99U))) || (a >= (1U) && b >= (0U) && b <= (99U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (99U) && u == b && !(v == ((a + u) + u))) || (a >= (1U) && b >= (0U) && b <= (99U) && u == b && v == ((a + u) + u))) && (!(u == (((b + v) + v) + v)) || (u == (((b + v) + v) + v) && !(v == a)) || (u == (((b + v) + v) + v) && v == a)) && (!(b >= (0U)) || (b >= (0U) && !(b <= (100U))) || (b >= (0U) && b <= (100U) && !(u == b)) || (b >= (0U) && b <= (100U) && u == b && !(v == a)) || (b >= (0U) && b <= (100U) && u == b && v == a)) && a >= (0U) && !(x >= (0U))) || (a <= (100U) && y >= (0U) && y <= (4294967295U) && !(x == y) && ((4294967295U) == y || (!((4294967295U) == y) && y == (4294967295U))) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (99U))) || (a >= (1U) && b >= (0U) && b <= (99U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (99U) && u == b && !(v == ((a + u) + u))) || (a >= (1U) && b >= (0U) && b <= (99U) && u == b && v == ((a + u) + u))) && (!(u == (((b + v) + v) + v)) || (u == (((b + v) + v) + v) && !(v == a)) || (u == (((b + v) + v) + v) && v == a && !(x <= (100U))) || (u == (((b + v) + v) + v) && v == a && x <= (100U) && !(y == x))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (100U))) || (b >= (0U) && b <= (100U) && !(u == b)) || (b >= (0U) && b <= (100U) && u == b && !(v == a)) || (b >= (0U) && b <= (100U) && u == b && v == a && !(x <= (100U))) || (b >= (0U) && b <= (100U) && u == b && v == a && x <= (100U) && !(y == b))) && a >= (0U) && x >= (0U) && !(x <= (4294967295U))) (../plain/lcm2_valuebound100.c:41:13)
[Info][Witness] unassume invariant: ((((((a <= 100U && a >= 0U) && ! (y == 4294967295U)) || (((a <= 100U && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || ((((a <= 100U && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((((((a <= 100U && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && a >= 1U) && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 99U)) || (((((a <= 100U && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 99U))) || (((a >= 1U && b >= 0U) && b <= 99U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 99U)))) && a >= 0U)) && ((((((a <= 100U && a >= 0U) && ! (y == 4294967295U)) || (((a <= 100U && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || ((((a <= 100U && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((((((a <= 100U && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && a >= 1U) && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 99U)) || (((((a <= 100U && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 99U))) || (((a >= 1U && b >= 0U) && b <= 99U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 99U)))) && a >= 0U)) (../plain/lcm2_valuebound100.c:35:5-35:10)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound100.c:38:9-38:46)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/lcm2_valuebound100.c:47:13-47:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound100.c:48:13-48:22)
[Info][Witness] unassume invariant: ((((((a <= 100U && a >= 0U) && ! (y == 4294967295U)) || (((a <= 100U && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || ((((a <= 100U && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((((((a <= 100U && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && a >= 1U) && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 99U)) || (((((a <= 100U && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 99U))) || (((a >= 1U && b >= 0U) && b <= 99U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 99U)))) && a >= 0U)) && ((((((a <= 100U && a >= 0U) && ! (y == 4294967295U)) || (((a <= 100U && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || ((((a <= 100U && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((((((a <= 100U && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && a >= 1U) && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 99U)) || (((((a <= 100U && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 99U))) || (((a >= 1U && b >= 0U) && b <= 99U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 99U)))) && a >= 0U)) (../plain/lcm2_valuebound100.c:48:13-48:22)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/lcm2_valuebound100.c:44:13-44:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound100.c:45:13-45:22)
[Info][Witness] unassume invariant: ((((((a <= 100U && a >= 0U) && ! (y == 4294967295U)) || (((a <= 100U && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || ((((a <= 100U && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((((((a <= 100U && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && a >= 1U) && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 99U)) || (((((a <= 100U && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 99U))) || (((a >= 1U && b >= 0U) && b <= 99U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 99U)))) && a >= 0U)) && ((((((a <= 100U && a >= 0U) && ! (y == 4294967295U)) || (((a <= 100U && y == 4294967295U) && a >= 0U) && ! (y >= 0U))) || ((((a <= 100U && y == 4294967295U) && a >= 0U) && y >= 0U) && ! (y <= 4294967295U))) || (((((((((a <= 100U && (! (a >= 0U) || (a >= 0U && y == 4294967295U))) && (! (a >= 0U) || (a >= 0U && y <= 4294967295U))) && a >= 1U) && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && y >= 0U) && y <= 99U)) || (((((a <= 100U && y == 4294967295U) && y >= 0U) && y <= 4294967295U) && (((((! (a >= 1U) || (a >= 1U && ! (b >= 0U))) || ((a >= 1U && b >= 0U) && ! (b <= 99U))) || (((a >= 1U && b >= 0U) && b <= 99U) && ! (u == b))) || ((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && ! (v == ((a + u) + u) + u))) || (((((a >= 1U && b >= 0U) && b <= 99U) && u == b) && v == ((a + u) + u) + u) && ! (y <= 99U)))) && a >= 0U)) (../plain/lcm2_valuebound100.c:45:13-45:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/lcm2_valuebound100.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_valuebound100.c:25:5-25:40)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/lcm2_valuebound100.c:37:12-37:13)
[Warning][Deadcode][CWE-571] condition 'a >= 0U' (possibly inserted by CIL) is always true (../plain/lcm2_valuebound100.c:23:5-23:40)
../plain/lcm2_valuebound100.c:16: Error: Cannot resolve variable cond.
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow
[Warning][Witness] invariant unconfirmed: (a <= (100U) && a >= (0U) && !(y == (4294967295U))) || (a <= (100U) && y == (4294967295U) && a >= (0U) && !(y >= (0U))) || (a <= (100U) && y == (4294967295U) && a >= (0U) && y >= (0U) && !(y <= (4294967295U))) || (a <= (100U) && (!(a >= (0U)) || (a >= (0U) && y == (4294967295U))) && (!(a >= (0U)) || (a >= (0U) && y <= (4294967295U))) && a >= (1U) && b >= (0U) && b <= (99U) && u == b && v == (((a + u) + u) + u) && y >= (0U) && y <= (99U)) || (a <= (100U) && y == (4294967295U) && y >= (0U) && y <= (4294967295U) && (!(a >= (1U)) || (a >= (1U) && !(b >= (0U))) || (a >= (1U) && b >= (0U) && !(b <= (99U))) || (a >= (1U) && b >= (0U) && b <= (99U) && !(u == b)) || (a >= (1U) && b >= (0U) && b <= (99U) && u == b && !(v == (((a + u) + u) + u))) || (a >= (1U) && b >= (0U) && b <= (99U) && u == b && v == (((a + u) + u) + u) && !(y <= (99U)))) && a >= (0U)) (../plain/lcm2_valuebound100.c:37:5)
[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:
../plain/lcm2_valuebound100.c:16: Error: Cannot resolve variable cond.
                                  cputime   walltime   allocated   count
Default                            1.622s     1.664s    152.66MB      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.004s     0.004s      3.34MB      1×
  analysis                           1.580s     1.622s    135.40MB      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      0.73MB      6×
    Cabs2cil                           0.002s     0.002s      1.19MB      6×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            1.447s     1.448s    117.86MB      1×
      S.Dom.equal                        0.001s     0.001s      0.05MB    130×
      base unassume                      0.075s     0.075s     56.84MB     16×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.100s     0.100s     16.65MB      1×
        postsolver_iter                    0.100s     0.100s     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×
