/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --enable witness.enabled --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/apache-escape-absolute.i.v+cfa-reducer.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][Integer > Overflow][CWE-190] Signed integer overflow (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2-314:25)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/apache-escape-absolute.i.v+cfa-reducer.c:6:1-8:1)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 85..86 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:85-86)
  on lines 97..98 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:97-98)
  on lines 113..114 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:113-114)
  on lines 125..126 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:125-126)
  on lines 145..146 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:145-146)
  on lines 157..158 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:157-158)
  on lines 177..178 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:177-178)
  on lines 189..190 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:189-190)
  on lines 214..215 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:214-215)
  on lines 226..227 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:226-227)
  on lines 255..256 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:255-256)
  on lines 272..273 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:272-273)
  on lines 284..285 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:284-285)
  on lines 308..309 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:308-309)
  on lines 374..375 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:374-375)
  on lines 386..387 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:386-387)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 108
  dead: 34 (2 in uncalled functions)
  total lines: 142
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___12 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:282:6-282:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:83:6-83:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___14 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:306:6-306:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___0 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:95:6-95:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___1 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:111:6-111:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___15 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:372:6-372:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___2 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:123:6-123:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___16 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:384:6-384:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___3 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:143:6-143:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___4 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:155:6-155:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___5 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:175:6-175:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___6 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:187:6-187:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___7 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:212:6-212:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___8 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:224:6-224:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___10 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:253:6-253:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___11 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:270:6-270:34)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 791

vars = 216    evals = 325    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            2.230s     2.240s    586.73MB      1×
  preprocess                         0.038s     0.046s      0.01MB      1×
  FrontC                             0.009s     0.009s      4.70MB      4×
  Cabs2cil                           0.008s     0.008s      5.37MB      4×
  mergeCIL                           0.003s     0.003s      3.41MB      1×
  analysis                           2.166s     2.167s    568.21MB      1×
    createCFG                          0.001s     0.001s      0.96MB      1×
      handle                             0.001s     0.001s      0.20MB     33×
      iter_connect                       0.001s     0.001s      0.62MB     33×
        computeSCCs                        0.001s     0.001s      0.41MB     34×
    global_inits                       0.001s     0.001s      0.27MB      1×
    solving                            1.801s     1.801s    232.05MB      1×
      S.Dom.equal                        0.001s     0.002s      0.11MB    327×
      cheap_full_reach                   0.001s     0.001s      0.08MB      1×
      postsolver                         0.687s     0.687s     75.99MB      1×
        postsolver_iter                    0.686s     0.686s     75.52MB      1×
    warn_global                        0.004s     0.004s      3.05MB      1×
    witness                            0.217s     0.217s    210.06MB      1×
      determine                          0.001s     0.001s      0.42MB      1×
      write                              0.217s     0.217s    209.64MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
