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


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: ((((((2U == y && x == 1U) || (((((! (2U == y) || (2U == y && ! (x == 1U))) && 6U <= x) && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && 64U == y)) || (((((! (2U == y) || (2U == y && ! (x == 1U))) && (((! (6U <= x) || (6U <= x && ! ((long long )x / 4294967296LL <= 0LL))) || ((6U <= x && (long long )x / 4294967296LL <= 0LL) && ! ((4294967295LL + (long long )x) % 4294967296LL < 6LL))) || (((6U <= x && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && ! (64U == y)))) && 5U <= x) && x <= 5U) && 32U == y)) || ((((((! (2U == y) || (2U == y && ! (x == 1U))) && (((! (6U <= x) || (6U <= x && ! ((long long )x / 4294967296LL <= 0LL))) || ((6U <= x && (long long )x / 4294967296LL <= 0LL) && ! ((4294967295LL + (long long )x) % 4294967296LL < 6LL))) || (((6U <= x && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && ! (64U == y)))) && ((! (5U <= x) || (5U <= x && ! (x <= 5U))) || ((5U <= x && x <= 5U) && ! (32U == y)))) && x <= 3U) && y == 8U) && 3U <= x)) || ((((((! (2U == y) || (2U == y && ! (x == 1U))) && (((! (6U <= x) || (6U <= x && ! ((long long )x / 4294967296LL <= 0LL))) || ((6U <= x && (long long )x / 4294967296LL <= 0LL) && ! ((4294967295LL + (long long )x) % 4294967296LL < 6LL))) || (((6U <= x && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && ! (64U == y)))) && ((! (5U <= x) || (5U <= x && ! (x <= 5U))) || ((5U <= x && x <= 5U) && ! (32U == y)))) && ((! (x <= 3U) || (x <= 3U && ! (y == 8U))) || ((x <= 3U && y == 8U) && ! (3U <= x)))) && y == 1U) && x == 0U)) || ((((((((! (2U == y) || (2U == y && ! (x == 1U))) && (((! (6U <= x) || (6U <= x && ! ((long long )x / 4294967296LL <= 0LL))) || ((6U <= x && (long long )x / 4294967296LL <= 0LL) && ! ((4294967295LL + (long long )x) % 4294967296LL < 6LL))) || (((6U <= x && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && ! (64U == y)))) && ((! (5U <= x) || (5U <= x && ! (x <= 5U))) || ((5U <= x && x <= 5U) && ! (32U == y)))) && ((! (x <= 3U) || (x <= 3U && ! (y == 8U))) || ((x <= 3U && y == 8U) && ! (3U <= x)))) && (! (y == 1U) || (y == 1U && ! (x == 0U)))) && 2U <= x) && y == 4U) && x <= 2U)) || (((((((((! (2U == y) || (2U == y && ! (x == 1U))) && (((! (6U <= x) || (6U <= x && ! ((long long )x / 4294967296LL <= 0LL))) || ((6U <= x && (long long )x / 4294967296LL <= 0LL) && ! ((4294967295LL + (long long )x) % 4294967296LL < 6LL))) || (((6U <= x && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && ! (64U == y)))) && ((! (5U <= x) || (5U <= x && ! (x <= 5U))) || ((5U <= x && x <= 5U) && ! (32U == y)))) && ((! (x <= 3U) || (x <= 3U && ! (y == 8U))) || ((x <= 3U && y == 8U) && ! (3U <= x)))) && (! (y == 1U) || (y == 1U && ! (x == 0U)))) && ((! (2U <= x) || (2U <= x && ! (y == 4U))) || ((2U <= x && y == 4U) && ! (x <= 2U)))) && 16U == y) && x <= 4U) && 4U <= x) (../plain/underapprox_1-2.c:14:16-14:21)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/underapprox_1-2.c:18:5-18:11)
[Info][Witness] unassume invariant: ((((((2U == y && x == 1U) || (((((! (2U == y) || (2U == y && ! (x == 1U))) && 6U <= x) && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && 64U == y)) || (((((! (2U == y) || (2U == y && ! (x == 1U))) && (((! (6U <= x) || (6U <= x && ! ((long long )x / 4294967296LL <= 0LL))) || ((6U <= x && (long long )x / 4294967296LL <= 0LL) && ! ((4294967295LL + (long long )x) % 4294967296LL < 6LL))) || (((6U <= x && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && ! (64U == y)))) && 5U <= x) && x <= 5U) && 32U == y)) || ((((((! (2U == y) || (2U == y && ! (x == 1U))) && (((! (6U <= x) || (6U <= x && ! ((long long )x / 4294967296LL <= 0LL))) || ((6U <= x && (long long )x / 4294967296LL <= 0LL) && ! ((4294967295LL + (long long )x) % 4294967296LL < 6LL))) || (((6U <= x && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && ! (64U == y)))) && ((! (5U <= x) || (5U <= x && ! (x <= 5U))) || ((5U <= x && x <= 5U) && ! (32U == y)))) && x <= 3U) && y == 8U) && 3U <= x)) || ((((((! (2U == y) || (2U == y && ! (x == 1U))) && (((! (6U <= x) || (6U <= x && ! ((long long )x / 4294967296LL <= 0LL))) || ((6U <= x && (long long )x / 4294967296LL <= 0LL) && ! ((4294967295LL + (long long )x) % 4294967296LL < 6LL))) || (((6U <= x && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && ! (64U == y)))) && ((! (5U <= x) || (5U <= x && ! (x <= 5U))) || ((5U <= x && x <= 5U) && ! (32U == y)))) && ((! (x <= 3U) || (x <= 3U && ! (y == 8U))) || ((x <= 3U && y == 8U) && ! (3U <= x)))) && y == 1U) && x == 0U)) || ((((((((! (2U == y) || (2U == y && ! (x == 1U))) && (((! (6U <= x) || (6U <= x && ! ((long long )x / 4294967296LL <= 0LL))) || ((6U <= x && (long long )x / 4294967296LL <= 0LL) && ! ((4294967295LL + (long long )x) % 4294967296LL < 6LL))) || (((6U <= x && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && ! (64U == y)))) && ((! (5U <= x) || (5U <= x && ! (x <= 5U))) || ((5U <= x && x <= 5U) && ! (32U == y)))) && ((! (x <= 3U) || (x <= 3U && ! (y == 8U))) || ((x <= 3U && y == 8U) && ! (3U <= x)))) && (! (y == 1U) || (y == 1U && ! (x == 0U)))) && 2U <= x) && y == 4U) && x <= 2U)) || (((((((((! (2U == y) || (2U == y && ! (x == 1U))) && (((! (6U <= x) || (6U <= x && ! ((long long )x / 4294967296LL <= 0LL))) || ((6U <= x && (long long )x / 4294967296LL <= 0LL) && ! ((4294967295LL + (long long )x) % 4294967296LL < 6LL))) || (((6U <= x && (long long )x / 4294967296LL <= 0LL) && (4294967295LL + (long long )x) % 4294967296LL < 6LL) && ! (64U == y)))) && ((! (5U <= x) || (5U <= x && ! (x <= 5U))) || ((5U <= x && x <= 5U) && ! (32U == y)))) && ((! (x <= 3U) || (x <= 3U && ! (y == 8U))) || ((x <= 3U && y == 8U) && ! (3U <= x)))) && (! (y == 1U) || (y == 1U && ! (x == 0U)))) && ((! (2U <= x) || (2U <= x && ! (y == 4U))) || ((2U <= x && y == 4U) && ! (x <= 2U)))) && 16U == y) && x <= 4U) && 4U <= x) (../plain/underapprox_1-2.c:18:5-18:11)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 13
  dead: 0
  total lines: 13
[Warning][Witness] invariant unconfirmed: ((2) == y && x == (1)) || ((!((2) == y) || ((2) == y && !(x == (1)))) && (6) <= x && (x / (4294967296LL)) <= (0) && (((4294967295LL) + x) % (4294967296LL)) < (6) && (64) == y) || ((!((2) == y) || ((2) == y && !(x == (1)))) && (!((6) <= x) || ((6) <= x && !((x / (4294967296LL)) <= (0))) || ((6) <= x && (x / (4294967296LL)) <= (0) && !((((4294967295LL) + x) % (4294967296LL)) < (6))) || ((6) <= x && (x / (4294967296LL)) <= (0) && (((4294967295LL) + x) % (4294967296LL)) < (6) && !((64) == y))) && (5) <= x && x <= (5) && (32) == y) || ((!((2) == y) || ((2) == y && !(x == (1)))) && (!((6) <= x) || ((6) <= x && !((x / (4294967296LL)) <= (0))) || ((6) <= x && (x / (4294967296LL)) <= (0) && !((((4294967295LL) + x) % (4294967296LL)) < (6))) || ((6) <= x && (x / (4294967296LL)) <= (0) && (((4294967295LL) + x) % (4294967296LL)) < (6) && !((64) == y))) && (!((5) <= x) || ((5) <= x && !(x <= (5))) || ((5) <= x && x <= (5) && !((32) == y))) && x <= (3) && y == (8) && (3) <= x) || ((!((2) == y) || ((2) == y && !(x == (1)))) && (!((6) <= x) || ((6) <= x && !((x / (4294967296LL)) <= (0))) || ((6) <= x && (x / (4294967296LL)) <= (0) && !((((4294967295LL) + x) % (4294967296LL)) < (6))) || ((6) <= x && (x / (4294967296LL)) <= (0) && (((4294967295LL) + x) % (4294967296LL)) < (6) && !((64) == y))) && (!((5) <= x) || ((5) <= x && !(x <= (5))) || ((5) <= x && x <= (5) && !((32) == y))) && (!(x <= (3)) || (x <= (3) && !(y == (8))) || (x <= (3) && y == (8) && !((3) <= x))) && y == (1) && x == (0)) || ((!((2) == y) || ((2) == y && !(x == (1)))) && (!((6) <= x) || ((6) <= x && !((x / (4294967296LL)) <= (0))) || ((6) <= x && (x / (4294967296LL)) <= (0) && !((((4294967295LL) + x) % (4294967296LL)) < (6))) || ((6) <= x && (x / (4294967296LL)) <= (0) && (((4294967295LL) + x) % (4294967296LL)) < (6) && !((64) == y))) && (!((5) <= x) || ((5) <= x && !(x <= (5))) || ((5) <= x && x <= (5) && !((32) == y))) && (!(x <= (3)) || (x <= (3) && !(y == (8))) || (x <= (3) && y == (8) && !((3) <= x))) && (!(y == (1)) || (y == (1) && !(x == (0)))) && (2) <= x && y == (4) && x <= (2)) || ((!((2) == y) || ((2) == y && !(x == (1)))) && (!((6) <= x) || ((6) <= x && !((x / (4294967296LL)) <= (0))) || ((6) <= x && (x / (4294967296LL)) <= (0) && !((((4294967295LL) + x) % (4294967296LL)) < (6))) || ((6) <= x && (x / (4294967296LL)) <= (0) && (((4294967295LL) + x) % (4294967296LL)) < (6) && !((64) == y))) && (!((5) <= x) || ((5) <= x && !(x <= (5))) || ((5) <= x && x <= (5) && !((32) == y))) && (!(x <= (3)) || (x <= (3) && !(y == (8))) || (x <= (3) && y == (8) && !((3) <= x))) && (!(y == (1)) || (y == (1) && !(x == (0)))) && (!((2) <= x) || ((2) <= x && !(y == (4))) || ((2) <= x && y == (4) && !(x <= (2)))) && (16) == y && x <= (4) && (4) <= x) (../plain/underapprox_1-2.c:16: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 = 23    evals = 31    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                            0.301s     0.314s    118.48MB      1×
  preprocess                         0.033s     0.032s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.05MB      4×
  Cabs2cil                           0.006s     0.006s      4.64MB      4×
  mergeCIL                           0.004s     0.004s      3.32MB      1×
  analysis                           0.249s     0.263s    101.54MB      1×
    createCFG                          0.001s     0.001s      0.58MB      1×
      handle                             0.001s     0.001s      0.08MB     33×
      iter_connect                       0.001s     0.001s      0.39MB     33×
        computeSCCs                        0.001s     0.001s      0.22MB     34×
    FrontC                             0.002s     0.002s      1.21MB      2×
    Cabs2cil                           0.002s     0.002s      1.20MB      2×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            0.145s     0.146s     85.09MB      1×
      S.Dom.equal                        0.001s     0.001s      0.02MB     32×
      base unassume                      0.054s     0.054s     67.65MB     11×
      cheap_full_reach                   0.001s     0.001s      0.01MB      1×
      postsolver                         0.004s     0.004s      4.32MB      1×
        postsolver_iter                    0.004s     0.004s      4.29MB      1×
    warn_global                        0.001s     0.001s      0.05MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
