./goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-location/convert-tmp.2023-02-16_10-47-42.files/cpachecker/mine-tutorial-ex4.6.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-location/convert-tmp.2023-02-16_10-47-42.files/cpachecker/mine-tutorial-ex4.6.yml/witness.yml --sets ana.specification /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/properties/unreach-call.prp --sets exp.architecture 64bit /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i


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


--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: x == (37) || x == (36) || x == (1) || x == (24) || x == (23) || x == (33) || x == (17) || x == (26) || x == (10) || x == (25) || x == (19) || x == (2) || x == (38) || x == (29) || x == (7) || x == (28) || x == (9) || x == (35) || x == (13) || x == (22) || x == (5) || x == (34) || x == (14) || x == (30) || x == (27) || x == (4) || x == (32) || x == (16) || x == (39) || x == (18) || x == (31) || x == (21) || x == (20) || x == (8) || x == (3) || x == (15) || x == (12) || x == (40) || (!(x == (40)) && x == (6)) || (!(x == (40)) && x == (11)) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i:17:5)
[Warning][Witness] couldn't locate invariant: x == (0) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i:21:3)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((x == 19 || x == 28) || x == 16) || x == 9) || x == 7) || x == 3) || x == 32) || x == 20) || x == 21) || x == 24) || x == 23) || x == 35) || x == 37) || x == 30) || x == 5) || x == 12) || x == 33) || x == 17) || x == 8) || x == 40) || (! (x == 40) && x == 31)) || (! (x == 40) && x == 26)) || (! (x == 40) && x == 10)) || (! (x == 40) && x == 25)) || (! (x == 40) && x == 1)) || (! (x == 40) && x == 27)) || (! (x == 40) && x == 14)) || (! (x == 40) && x == 34)) || (! (x == 40) && x == 13)) || (! (x == 40) && x == 22)) || (! (x == 40) && x == 0)) || (! (x == 40) && x == 6)) || (! (x == 40) && x == 29)) || (! (x == 40) && x == 18)) || (! (x == 40) && x == 2)) || (! (x == 40) && x == 39)) || (! (x == 40) && x == 11)) || (! (x == 40) && x == 38)) || (! (x == 40) && x == 15)) || (! (x == 40) && x == 4)) || (! (x == 40) && x == 36) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i:15:7-15:13)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((x == 19 || x == 28) || x == 16) || x == 9) || x == 7) || x == 3) || x == 32) || x == 20) || x == 21) || x == 24) || x == 23) || x == 35) || x == 37) || x == 30) || x == 5) || x == 12) || x == 33) || x == 17) || x == 8) || x == 40) || (! (x == 40) && x == 31)) || (! (x == 40) && x == 26)) || (! (x == 40) && x == 10)) || (! (x == 40) && x == 25)) || (! (x == 40) && x == 1)) || (! (x == 40) && x == 27)) || (! (x == 40) && x == 14)) || (! (x == 40) && x == 34)) || (! (x == 40) && x == 13)) || (! (x == 40) && x == 22)) || (! (x == 40) && x == 0)) || (! (x == 40) && x == 6)) || (! (x == 40) && x == 29)) || (! (x == 40) && x == 18)) || (! (x == 40) && x == 2)) || (! (x == 40) && x == 39)) || (! (x == 40) && x == 11)) || (! (x == 40) && x == 38)) || (! (x == 40) && x == 15)) || (! (x == 40) && x == 4)) || (! (x == 40) && x == 36) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i:19:5-19:30)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i:12:1-12:172)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 9
  dead: 1 (1 in uncalled functions)
  total lines: 10
[Warning][Deadcode][CWE-570] condition '! cond' is always false (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i:13:39-13:46)
[Warning][Witness] invariant unconfirmed: x == (19) || x == (28) || x == (16) || x == (9) || x == (7) || x == (3) || x == (32) || x == (20) || x == (21) || x == (24) || x == (23) || x == (35) || x == (37) || x == (30) || x == (5) || x == (12) || x == (33) || x == (17) || x == (8) || x == (40) || (!(x == (40)) && x == (31)) || (!(x == (40)) && x == (26)) || (!(x == (40)) && x == (10)) || (!(x == (40)) && x == (25)) || (!(x == (40)) && x == (1)) || (!(x == (40)) && x == (27)) || (!(x == (40)) && x == (14)) || (!(x == (40)) && x == (34)) || (!(x == (40)) && x == (13)) || (!(x == (40)) && x == (22)) || (!(x == (40)) && x == (0)) || (!(x == (40)) && x == (6)) || (!(x == (40)) && x == (29)) || (!(x == (40)) && x == (18)) || (!(x == (40)) && x == (2)) || (!(x == (40)) && x == (39)) || (!(x == (40)) && x == (11)) || (!(x == (40)) && x == (38)) || (!(x == (40)) && x == (15)) || (!(x == (40)) && x == (4)) || (!(x == (40)) && x == (36)) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i:16:3)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 1
  refuted: 0
  error: 2
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 3
SV-COMP result: unknown

vars = 19    evals = 50    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            0.237s     0.238s     74.70MB      1×
  preprocess                         0.026s     0.025s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.10MB      4×
  Cabs2cil                           0.005s     0.006s      4.69MB      4×
  mergeCIL                           0.003s     0.003s      3.33MB      1×
  analysis                           0.194s     0.194s     57.63MB      1×
    createCFG                          0.001s     0.001s      0.59MB      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.001s     0.001s      0.42MB      2×
    Cabs2cil                           0.001s     0.001s      0.53MB      2×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            0.066s     0.066s     40.21MB      1×
      S.Dom.equal                        0.001s     0.001s      0.02MB     52×
      base unassume                      0.025s     0.025s     23.47MB      9×
      cheap_full_reach                   0.001s     0.001s      0.01MB      1×
      postsolver                         0.004s     0.004s      3.35MB      1×
        postsolver_iter                    0.004s     0.004s      3.33MB      1×
    warn_global                        0.001s     0.001s      0.07MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
