/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/egcd3-ll_valuebound10.yml.witness.yml --witness.yaml.validate cbmc/egcd3-ll_valuebound10.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/egcd3-ll_valuebound10.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: ((((r == 0LL && q == 0LL) && a == (long long )x) && p == 1LL) && b == (long long )y) && s == 1LL (../plain/egcd3-ll_valuebound10.c:33:5-33:10)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound10.c:55:21-55:34)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/egcd3-ll_valuebound10.c:57:17-57:26)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound10.c:58:17-58:26)
[Info][Witness] unassume invariant: d == 1LL && v == b (../plain/egcd3-ll_valuebound10.c:58:17-58:26)
[Info][Witness] unassume invariant: d == 1LL && v == b (../plain/egcd3-ll_valuebound10.c:47:13-47:18)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound10.c:50:17-50:54)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound10.c:51:17-51:54)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound10.c:52:17-52:50)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound10.c:53:17-53:46)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound10.c:60:13-60:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/egcd3-ll_valuebound10.c:61:13-61:22)
[Info][Witness] unassume invariant: k == 0LL && c == a (../plain/egcd3-ll_valuebound10.c:61:13-61:22)
[Info][Witness] unassume invariant: k == 0LL && c == a (../plain/egcd3-ll_valuebound10.c:40:9-40:14)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound10.c:69:9-69:25)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound10.c:72:9-72:25)
[Info][Witness] unassume invariant: ((((r == 0LL && q == 0LL) && a == (long long )x) && p == 1LL) && b == (long long )y) && s == 1LL (../plain/egcd3-ll_valuebound10.c:72:9-72:25)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound10.c:74:5-74:50)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 50
  dead: 0
  total lines: 50
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/egcd3-ll_valuebound10.c:35:12-35:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/egcd3-ll_valuebound10.c:42:16-42:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/egcd3-ll_valuebound10.c:49:20-49:21)
[Warning][Witness] invariant unconfirmed: v == b (../plain/egcd3-ll_valuebound10.c:49:13)
[Warning][Witness] invariant unconfirmed: s == (1LL) (../plain/egcd3-ll_valuebound10.c:35:5)
[Warning][Witness] invariant unconfirmed: b == ((signed long long int)y) (../plain/egcd3-ll_valuebound10.c:30:5)
[Warning][Witness] invariant unconfirmed: p == (1LL) (../plain/egcd3-ll_valuebound10.c:31:5)
[Warning][Witness] invariant unconfirmed: d == (1LL) (../plain/egcd3-ll_valuebound10.c:47:13)
[Warning][Witness] invariant unconfirmed: c == a (../plain/egcd3-ll_valuebound10.c:40:9)
[Warning][Witness] invariant unconfirmed: a == ((signed long long int)x) (../plain/egcd3-ll_valuebound10.c:29:5)
[Warning][Witness] invariant unconfirmed: k == (0LL) (../plain/egcd3-ll_valuebound10.c:42:9)
[Warning][Witness] invariant unconfirmed: q == (0LL) (../plain/egcd3-ll_valuebound10.c:32:5)
[Warning][Witness] invariant unconfirmed: r == (0LL) (../plain/egcd3-ll_valuebound10.c:33:5)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 10
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 10
SV-COMP result: unknown

vars = 101    evals = 655    narrow_reuses = 26

Timings:
                                  cputime   walltime   allocated   count
Default                            0.539s     0.539s    301.03MB      1×
  preprocess                         0.024s     0.023s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.20MB      4×
  Cabs2cil                           0.005s     0.005s      4.89MB      4×
  mergeCIL                           0.003s     0.003s      3.36MB      1×
  analysis                           0.498s     0.498s    283.53MB      1×
    createCFG                          0.001s     0.001s      0.71MB      1×
      handle                             0.001s     0.001s      0.13MB     34×
      iter_connect                       0.001s     0.001s      0.46MB     34×
        computeSCCs                        0.001s     0.001s      0.28MB     35×
    FrontC                             0.001s     0.001s      0.13MB     20×
    Cabs2cil                           0.007s     0.007s      1.85MB     20×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            0.478s     0.478s    268.85MB      1×
      S.Dom.equal                        0.001s     0.002s      0.23MB    681×
      base unassume                      0.009s     0.010s     13.93MB     85×
      cheap_full_reach                   0.001s     0.001s      0.04MB      1×
      postsolver                         0.048s     0.048s     23.53MB      1×
        postsolver_iter                    0.048s     0.048s     23.45MB      1×
    warn_global                        0.001s     0.001s      0.26MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
