/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 cbmc/eureka_01-2.yml.witness.yml --witness.yaml.validate cbmc/eureka_01-2.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/eureka_01-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())) )
[Warning][Witness] couldn't locate invariant: i == (0) || i == (1) || i == (2) || i == (3) || i == (4) || i == (5) (../plain/eureka_01-2.c:57:7)
[Warning][Witness] couldn't locate invariant: i == (0) || i == (1) || i == (2) || i == (3) || i == (4) || i == (5) (../plain/eureka_01-2.c:60:3)
[Info][Witness] unassume invariant: (((((((((((((((((Weight[5] == 5 && Weight[4] == 4) && Weight[3] == 3) && Weight[2] == 2) && Weight[1] == 1) && Weight[0] == 0) && Weight[13] == 13) && Weight[12] == 12) && Weight[11] == 11) && Weight[10] == 10) && Weight[9] == 9) && Weight[8] == 8) && Weight[7] == 7) && Weight[6] == 6) && (((((((((((((Dest[2] == 4 && Dest[3] == 1) && Dest[0] == 1) && Dest[1] == 3) && Dest[10] == 0) && Dest[11] == 0) && Dest[8] == 3) && Dest[9] == 0) && Dest[6] == 3) && Dest[7] == 4) && Dest[4] == 1) && Dest[5] == 4) && Dest[12] == 0) && Dest[13] == 2)) && (((((Source[2] == 1 && Source[1] == 4) && Source[0] == 0) && Source[5] == 0) && Source[4] == 0) && Source[3] == 1)) && nodecount == 5) && edgecount == 20) && source == 0 (../plain/eureka_01-2.c:24:6-24:32)
[Info][Witness] unassume invariant: (((((((((((((((((Weight[5] == 5 && Weight[4] == 4) && Weight[3] == 3) && Weight[2] == 2) && Weight[1] == 1) && Weight[0] == 0) && Weight[13] == 13) && Weight[12] == 12) && Weight[11] == 11) && Weight[10] == 10) && Weight[9] == 9) && Weight[8] == 8) && Weight[7] == 7) && Weight[6] == 6) && (((((((((((((Dest[2] == 4 && Dest[3] == 1) && Dest[0] == 1) && Dest[1] == 3) && Dest[10] == 0) && Dest[11] == 0) && Dest[8] == 3) && Dest[9] == 0) && Dest[6] == 3) && Dest[7] == 4) && Dest[4] == 1) && Dest[5] == 4) && Dest[12] == 0) && Dest[13] == 2)) && (((((Source[2] == 1 && Source[1] == 4) && Source[0] == 0) && Source[5] == 0) && Source[4] == 0) && Source[3] == 1)) && nodecount == 5) && edgecount == 20) && source == 0 (../plain/eureka_01-2.c:24:6-24:32)
[Info][Witness] unassume invariant: (((i == 0 || i == 1) || i == 2) || i == 3) || i == 5 (../plain/eureka_01-2.c:33:6-33:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/eureka_01-2.c:39:7-39:44)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/eureka_01-2.c:41:8-41:45)
[Info][Witness] unassume invariant: ((((i == 0 || i == 1) || i == 2) || i == 3) || i == 4) || i == 5 (../plain/eureka_01-2.c:35:10-35:36)
[Info][Witness] unassume invariant: ((((i == 0 || i == 1) || i == 2) || i == 3) || i == 4) || i == 5 (../plain/eureka_01-2.c:35:10-35:36)
[Info][Witness] unassume invariant: (((i == 0 || i == 1) || i == 2) || i == 3) || i == 5 (../plain/eureka_01-2.c:33:6-33:32)
[Info][Witness] unassume invariant: ((((((i == 0 || i == 1) || i == 2) || i == 3) || i == 4) || i == 5) && ((((((((((((((((((((j == 0 || j == 1) || j == 2) || j == 3) || j == 4) || j == 5) || j == 6) || j == 7) || j == 8) || j == 9) || j == 10) || j == 11) || j == 12) || j == 13) || j == 14) || j == 15) || j == 16) || j == 17) || j == 18) || j == 19) || j == 20)) && ((((x == 1 || x == 3) || x == 4) || x == 0) || x == 2) (../plain/eureka_01-2.c:45:6-45:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/eureka_01-2.c:49:10-49:47)
[Info][Witness] unassume invariant: ((((((i == 0 || i == 1) || i == 2) || i == 3) || i == 4) || i == 5) && ((((((((((((((((((((j == 0 || j == 1) || j == 2) || j == 3) || j == 4) || j == 5) || j == 6) || j == 7) || j == 8) || j == 9) || j == 10) || j == 11) || j == 12) || j == 13) || j == 14) || j == 15) || j == 16) || j == 17) || j == 18) || j == 19) || j == 20)) && ((((x == 1 || x == 3) || x == 4) || x == 0) || x == 2) (../plain/eureka_01-2.c:45:6-45:32)
[Info][Witness] unassume invariant: (((((((((((((((((((((i == 0 || i == 1) || i == 2) || i == 3) || i == 4) || i == 5) || i == 6) || i == 7) || i == 8) || i == 9) || i == 10) || i == 11) || i == 12) || i == 13) || i == 14) || i == 15) || i == 16) || i == 17) || i == 18) || i == 19) || i == 20) && ((((x == 1 || x == 3) || x == 4) || x == 0) || x == 2)) && ((((((((((((((((((((i == 0 || i == 1) || i == 2) || i == 3) || i == 4) || i == 5) || i == 6) || i == 7) || i == 8) || i == 9) || i == 10) || i == 11) || i == 12) || i == 13) || i == 14) || i == 15) || i == 16) || i == 17) || i == 18) || i == 19) || i == 20) (../plain/eureka_01-2.c:55:6-55:32)
[Info][Witness] unassume invariant: (((((((((((((((((((((i == 0 || i == 1) || i == 2) || i == 3) || i == 4) || i == 5) || i == 6) || i == 7) || i == 8) || i == 9) || i == 10) || i == 11) || i == 12) || i == 13) || i == 14) || i == 15) || i == 16) || i == 17) || i == 18) || i == 19) || i == 20) && ((((x == 1 || x == 3) || x == 4) || x == 0) || x == 2)) && ((((((((((((((((((((i == 0 || i == 1) || i == 2) || i == 3) || i == 4) || i == 5) || i == 6) || i == 7) || i == 8) || i == 9) || i == 10) || i == 11) || i == 12) || i == 13) || i == 14) || i == 15) || i == 16) || i == 17) || i == 18) || i == 19) || i == 20) (../plain/eureka_01-2.c:55:6-55:32)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (../plain/eureka_01-2.c:3:1-3:77)
[Warning][Deadcode] Function '__VERIFIER_assert' has dead code:
  on line 7 (../plain/eureka_01-2.c:7-7)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 28
  dead: 2 (1 in uncalled functions)
  total lines: 30
[Warning][Deadcode][CWE-570] condition '! cond' is always false (../plain/eureka_01-2.c:6:7-6:14)
[Warning][Witness] invariant unconfirmed: i == (0) || i == (1) || i == (2) || i == (3) || i == (4) || i == (5) || i == (6) || i == (7) || i == (8) || i == (9) || i == (10) || i == (11) || i == (12) || i == (13) || i == (14) || i == (15) || i == (16) || i == (17) || i == (18) || i == (19) || i == (20) (../plain/eureka_01-2.c:55:3)
[Warning][Witness] invariant unconfirmed: i == (0) || i == (1) || i == (2) || i == (3) || i == (4) || i == (5) (../plain/eureka_01-2.c:35:7)
[Warning][Witness] invariant unconfirmed: x == (1) || x == (3) || x == (4) || x == (0) || x == (2) (../plain/eureka_01-2.c:38:4)
[Success][Witness] invariant confirmed: source == (0) (../plain/eureka_01-2.c:17:3)
[Warning][Witness] invariant unconfirmed: i == (0) || i == (1) || i == (2) || i == (3) || i == (5) (../plain/eureka_01-2.c:33:3)
[Success][Witness] invariant confirmed: edgecount == (20) (../plain/eureka_01-2.c:16:3)
[Success][Witness] invariant confirmed: nodecount == (5) (../plain/eureka_01-2.c:15:3)
[Warning][Witness] invariant unconfirmed: j == (0) || j == (1) || j == (2) || j == (3) || j == (4) || j == (5) || j == (6) || j == (7) || j == (8) || j == (9) || j == (10) || j == (11) || j == (12) || j == (13) || j == (14) || j == (15) || j == (16) || j == (17) || j == (18) || j == (19) || j == (20) (../plain/eureka_01-2.c:37:4)
[Warning][Witness] invariant unconfirmed: x == (1) || x == (3) || x == (4) || x == (0) || x == (2) (../plain/eureka_01-2.c:48:7)
[Warning][Witness] invariant unconfirmed: (Source[2]) == (1) && (Source[1]) == (4) && (Source[0]) == (0) && (Source[5]) == (0) && (Source[4]) == (0) && (Source[3]) == (1) (../plain/eureka_01-2.c:18:3)
[Warning][Witness] invariant unconfirmed: (Dest[2]) == (4) && (Dest[3]) == (1) && (Dest[0]) == (1) && (Dest[1]) == (3) && (Dest[10]) == (0) && (Dest[11]) == (0) && (Dest[8]) == (3) && (Dest[9]) == (0) && (Dest[6]) == (3) && (Dest[7]) == (4) && (Dest[4]) == (1) && (Dest[5]) == (4) && (Dest[12]) == (0) && (Dest[13]) == (2) (../plain/eureka_01-2.c:19:3)
[Warning][Witness] invariant unconfirmed: i == (0) || i == (1) || i == (2) || i == (3) || i == (4) || i == (5) || i == (6) || i == (7) || i == (8) || i == (9) || i == (10) || i == (11) || i == (12) || i == (13) || i == (14) || i == (15) || i == (16) || i == (17) || i == (18) || i == (19) || i == (20) (../plain/eureka_01-2.c:47:7)
[Warning][Witness] invariant unconfirmed: (Weight[5]) == (5) && (Weight[4]) == (4) && (Weight[3]) == (3) && (Weight[2]) == (2) && (Weight[1]) == (1) && (Weight[0]) == (0) && (Weight[13]) == (13) && (Weight[12]) == (12) && (Weight[11]) == (11) && (Weight[10]) == (10) && (Weight[9]) == (9) && (Weight[8]) == (8) && (Weight[7]) == (7) && (Weight[6]) == (6) (../plain/eureka_01-2.c:20:3)
[Warning][Witness] invariant unconfirmed: i == (0) || i == (1) || i == (2) || i == (3) || i == (4) || i == (5) (../plain/eureka_01-2.c:45:3)
[Info][Witness] witness validation summary:
  confirmed: 3
  unconfirmed: 11
  refuted: 0
  error: 2
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 16
SV-COMP result: unknown

vars = 111    evals = 277    narrow_reuses = 10

Timings:
                                  cputime   walltime   allocated   count
Default                            0.677s     0.678s    374.47MB      1×
  preprocess                         0.023s     0.022s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.20MB      4×
  Cabs2cil                           0.005s     0.005s      4.95MB      4×
  mergeCIL                           0.003s     0.003s      3.35MB      1×
  analysis                           0.637s     0.638s    356.87MB      1×
    createCFG                          0.001s     0.001s      0.81MB      1×
      handle                             0.001s     0.001s      0.15MB     33×
      iter_connect                       0.001s     0.001s      0.53MB     33×
        computeSCCs                        0.001s     0.001s      0.34MB     34×
    FrontC                             0.002s     0.002s      0.88MB     28×
    Cabs2cil                           0.014s     0.014s      3.16MB     28×
    global_inits                       0.001s     0.001s      0.18MB      1×
    solving                            0.381s     0.381s    320.37MB      1×
      S.Dom.equal                        0.001s     0.001s      0.10MB    287×
      base unassume                      0.039s     0.039s     58.62MB     71×
      cheap_full_reach                   0.001s     0.001s      0.06MB      1×
      postsolver                         0.054s     0.054s     73.09MB      1×
        postsolver_iter                    0.054s     0.054s     73.00MB      1×
    warn_global                        0.001s     0.001s      0.18MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
