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


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


--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) && h == (0U) && n == (0U) && p == (0U) && q == (1U) && r == n) || (h == (0U) && r == n && p == (0U) && (!(counter == (2)) || (counter == (2) && !(n == (0U))) || (counter == (2) && n == (0U) && !(q == (1U)))) && counter == (4) && n >= (4U) && n <= (4294967295U) && q == (16U)) || (h == (0U) && r == n && p == (0U) && (!(counter == (2)) || (counter == (2) && !(n == (0U))) || (counter == (2) && n == (0U) && !(q == (1U)))) && (!(counter == (4)) || (counter == (4) && !(n >= (4U))) || (counter == (4) && n >= (4U) && !(n <= (4294967295U))) || (counter == (4) && n >= (4U) && n <= (4294967295U) && !(q == (16U)))) && counter == (3) && n >= (1U) && n <= (3U) && q == (4U)) (../plain/dijkstra-u_unwindbound2.c:47:13)
[Warning][Witness] couldn't locate invariant: counter == (2) && h == (0U) && n == (0U) && p == (0U) && q == (1U) && r == n (../plain/dijkstra-u_unwindbound2.c:39:9)
[Warning][Witness] couldn't locate invariant: (counter == (2) && h == (0U) && n == (0U) && p == (0U) && q == (1U) && r == n) || (h == (0U) && r == n && p == (0U) && (!(counter == (2)) || (counter == (2) && !(n == (0U))) || (counter == (2) && n == (0U) && !(q == (1U)))) && counter == (4) && n >= (4U) && n <= (4294967295U) && q == (16U)) || (h == (0U) && r == n && p == (0U) && (!(counter == (2)) || (counter == (2) && !(n == (0U))) || (counter == (2) && n == (0U) && !(q == (1U)))) && (!(counter == (4)) || (counter == (4) && !(n >= (4U))) || (counter == (4) && n >= (4U) && !(n <= (4294967295U))) || (counter == (4) && n >= (4U) && n <= (4294967295U) && !(q == (16U)))) && counter == (3) && n >= (1U) && n <= (3U) && q == (4U)) (../plain/dijkstra-u_unwindbound2.c:57:5)
[Info][Witness] unassume invariant: ((((((((h == 0U && p == 0U) && counter == 0) && q == 1U) && r == n) || ((((((h == 0U && p == 0U) && ((! (counter == 0) || (counter == 0 && ! (q == 1U))) || ((counter == 0 && q == 1U) && ! (r == n)))) && counter == 1) && ! (n == 0U)) && q == 4U) && ! (0U == n))) || ((((((((h == 0U && p == 0U) && (! (counter == 0) || (counter == 0 && ! (q == 1U)))) && (((! (counter == 1) || (counter == 1 && n == 0U)) || ((counter == 1 && ! (n == 0U)) && ! (q == 4U))) || (((counter == 1 && ! (n == 0U)) && q == 4U) && 0U == n))) && counter == 2) && n >= 4U) && n <= 4294967295U) && q == 16U) && r == n)) || (((((((h == 0U && p == 0U) && ! (counter == 0)) && ((n == 0U || (! (n == 0U) && ! (q == 4U))) || ((! (n == 0U) && q == 4U) && 0U == n))) && (((! (counter == 2) || (counter == 2 && ! (n >= 4U))) || ((counter == 2 && n >= 4U) && ! (n <= 4294967295U))) || (((counter == 2 && n >= 4U) && n <= 4294967295U) && ! (q == 16U)))) && counter == 1) && q == 1U) && r == n)) || ((((((((((h == 0U && p == 0U) && (! (counter == 0) || (counter == 0 && ! (q == 1U)))) && (((! (counter == 1) || (counter == 1 && n == 0U)) || ((counter == 1 && ! (n == 0U)) && ! (q == 4U))) || (((counter == 1 && ! (n == 0U)) && q == 4U) && 0U == n))) && ! (counter == 2)) && (! (counter == 1) || (counter == 1 && ! (q == 1U)))) && counter == 3) && n >= 4U) && n <= 4294967295U) && q == 16U) && r == n)) || (((((((((h == 0U && p == 0U) && ((! (counter == 0) || (counter == 0 && ! (q == 1U))) || ((counter == 0 && q == 1U) && ! (r == n)))) && ! (counter == 1)) && (((! (n >= 4U) || (n >= 4U && ! (n <= 4294967295U))) || ((n >= 4U && n <= 4294967295U) && ! (q == 16U))) || (((n >= 4U && n <= 4294967295U) && q == 16U) && ! (r == n)))) && ((((! (counter == 3) || (counter == 3 && ! (n >= 4U))) || ((counter == 3 && n >= 4U) && ! (n <= 4294967295U))) || (((counter == 3 && n >= 4U) && n <= 4294967295U) && ! (q == 16U))) || ((((counter == 3 && n >= 4U) && n <= 4294967295U) && q == 16U) && ! (r == n)))) && counter == 2) && ! (n == 0U)) && q == 4U) && ! (0U == n)) (../plain/dijkstra-u_unwindbound2.c:29:5-29:10)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/dijkstra-u_unwindbound2.c:34:9-34:18)
[Info][Witness] unassume invariant: ((((((((h == 0U && p == 0U) && counter == 0) && q == 1U) && r == n) || ((((((h == 0U && p == 0U) && ((! (counter == 0) || (counter == 0 && ! (q == 1U))) || ((counter == 0 && q == 1U) && ! (r == n)))) && counter == 1) && ! (n == 0U)) && q == 4U) && ! (0U == n))) || ((((((((h == 0U && p == 0U) && (! (counter == 0) || (counter == 0 && ! (q == 1U)))) && (((! (counter == 1) || (counter == 1 && n == 0U)) || ((counter == 1 && ! (n == 0U)) && ! (q == 4U))) || (((counter == 1 && ! (n == 0U)) && q == 4U) && 0U == n))) && counter == 2) && n >= 4U) && n <= 4294967295U) && q == 16U) && r == n)) || (((((((h == 0U && p == 0U) && ! (counter == 0)) && ((n == 0U || (! (n == 0U) && ! (q == 4U))) || ((! (n == 0U) && q == 4U) && 0U == n))) && (((! (counter == 2) || (counter == 2 && ! (n >= 4U))) || ((counter == 2 && n >= 4U) && ! (n <= 4294967295U))) || (((counter == 2 && n >= 4U) && n <= 4294967295U) && ! (q == 16U)))) && counter == 1) && q == 1U) && r == n)) || ((((((((((h == 0U && p == 0U) && (! (counter == 0) || (counter == 0 && ! (q == 1U)))) && (((! (counter == 1) || (counter == 1 && n == 0U)) || ((counter == 1 && ! (n == 0U)) && ! (q == 4U))) || (((counter == 1 && ! (n == 0U)) && q == 4U) && 0U == n))) && ! (counter == 2)) && (! (counter == 1) || (counter == 1 && ! (q == 1U)))) && counter == 3) && n >= 4U) && n <= 4294967295U) && q == 16U) && r == n)) || (((((((((h == 0U && p == 0U) && ((! (counter == 0) || (counter == 0 && ! (q == 1U))) || ((counter == 0 && q == 1U) && ! (r == n)))) && ! (counter == 1)) && (((! (n >= 4U) || (n >= 4U && ! (n <= 4294967295U))) || ((n >= 4U && n <= 4294967295U) && ! (q == 16U))) || (((n >= 4U && n <= 4294967295U) && q == 16U) && ! (r == n)))) && ((((! (counter == 3) || (counter == 3 && ! (n >= 4U))) || ((counter == 3 && n >= 4U) && ! (n <= 4294967295U))) || (((counter == 3 && n >= 4U) && n <= 4294967295U) && ! (q == 16U))) || ((((counter == 3 && n >= 4U) && n <= 4294967295U) && q == 16U) && ! (r == n)))) && counter == 2) && ! (n == 0U)) && q == 4U) && ! (0U == n)) (../plain/dijkstra-u_unwindbound2.c:34:9-34:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/dijkstra-u_unwindbound2.c:39:9-39:41)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/dijkstra-u_unwindbound2.c:40:9-40:44)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/dijkstra-u_unwindbound2.c:41:9-41:138)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/dijkstra-u_unwindbound2.c:41:9-41:138)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/dijkstra-u_unwindbound2.c:42:9-42:160)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/dijkstra-u_unwindbound2.c:42:9-42:160)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/dijkstra-u_unwindbound2.c:43:9-43:118)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/dijkstra-u_unwindbound2.c:43:9-43:118)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/dijkstra-u_unwindbound2.c:44:9-44:54)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/dijkstra-u_unwindbound2.c:44:9-44:54)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/dijkstra-u_unwindbound2.c:54:13-54:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/dijkstra-u_unwindbound2.c:38:12-38:23)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/dijkstra-u_unwindbound2.c:57:5-57:80)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/dijkstra-u_unwindbound2.c:57:5-57:80)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/dijkstra-u_unwindbound2.c:58:5-58:40)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/dijkstra-u_unwindbound2.c:58:5-58:40)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/dijkstra-u_unwindbound2.c:59:5-59:70)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/dijkstra-u_unwindbound2.c:59:5-59:70)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 37
  dead: 0
  total lines: 37
[Warning][Witness] invariant unconfirmed: (h == (0U) && p == (0U) && counter == (0) && q == (1U) && r == n) || (h == (0U) && p == (0U) && (!(counter == (0)) || (counter == (0) && !(q == (1U))) || (counter == (0) && q == (1U) && !(r == n))) && counter == (1) && !(n == (0U)) && q == (4U) && !((0U) == n)) || (h == (0U) && p == (0U) && (!(counter == (0)) || (counter == (0) && !(q == (1U)))) && (!(counter == (1)) || (counter == (1) && n == (0U)) || (counter == (1) && !(n == (0U)) && !(q == (4U))) || (counter == (1) && !(n == (0U)) && q == (4U) && (0U) == n)) && counter == (2) && n >= (4U) && n <= (4294967295U) && q == (16U) && r == n) || (h == (0U) && p == (0U) && !(counter == (0)) && (n == (0U) || (!(n == (0U)) && !(q == (4U))) || (!(n == (0U)) && q == (4U) && (0U) == n)) && (!(counter == (2)) || (counter == (2) && !(n >= (4U))) || (counter == (2) && n >= (4U) && !(n <= (4294967295U))) || (counter == (2) && n >= (4U) && n <= (4294967295U) && !(q == (16U)))) && counter == (1) && q == (1U) && r == n) || (h == (0U) && p == (0U) && (!(counter == (0)) || (counter == (0) && !(q == (1U)))) && (!(counter == (1)) || (counter == (1) && n == (0U)) || (counter == (1) && !(n == (0U)) && !(q == (4U))) || (counter == (1) && !(n == (0U)) && q == (4U) && (0U) == n)) && !(counter == (2)) && (!(counter == (1)) || (counter == (1) && !(q == (1U)))) && counter == (3) && n >= (4U) && n <= (4294967295U) && q == (16U) && r == n) || (h == (0U) && p == (0U) && (!(counter == (0)) || (counter == (0) && !(q == (1U))) || (counter == (0) && q == (1U) && !(r == n))) && !(counter == (1)) && (!(n >= (4U)) || (n >= (4U) && !(n <= (4294967295U))) || (n >= (4U) && n <= (4294967295U) && !(q == (16U))) || (n >= (4U) && n <= (4294967295U) && q == (16U) && !(r == n))) && (!(counter == (3)) || (counter == (3) && !(n >= (4U))) || (counter == (3) && n >= (4U) && !(n <= (4294967295U))) || (counter == (3) && n >= (4U) && n <= (4294967295U) && !(q == (16U))) || (counter == (3) && n >= (4U) && n <= (4294967295U) && q == (16U) && !(r == n))) && counter == (2) && !(n == (0U)) && q == (4U) && !((0U) == n)) (../plain/dijkstra-u_unwindbound2.c:30:5)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 1
  refuted: 0
  error: 3
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 4
SV-COMP result: unknown

vars = 93    evals = 341    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            1.345s     1.346s    281.40MB      1×
  preprocess                         0.026s     0.025s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.26MB      4×
  Cabs2cil                           0.005s     0.005s      5.11MB      4×
  mergeCIL                           0.003s     0.003s      3.36MB      1×
  analysis                           1.302s     1.302s    263.64MB      1×
    createCFG                          0.001s     0.001s      0.65MB      1×
      handle                             0.001s     0.001s      0.11MB     34×
      iter_connect                       0.001s     0.001s      0.43MB     34×
        computeSCCs                        0.001s     0.001s      0.25MB     35×
    FrontC                             0.002s     0.002s      0.81MB      2×
    Cabs2cil                           0.001s     0.001s      0.83MB      2×
    global_inits                       0.001s     0.001s      0.18MB      1×
    solving                            0.935s     0.935s    243.74MB      1×
      S.Dom.equal                        0.001s     0.002s      0.12MB    343×
      base unassume                      0.084s     0.085s     51.65MB     13×
      cheap_full_reach                   0.001s     0.001s      0.04MB      1×
      postsolver                         0.044s     0.044s     22.27MB      1×
        postsolver_iter                    0.044s     0.044s     22.19MB      1×
    warn_global                        0.001s     0.001s      0.19MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
