/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 graves-cpa/count_up_down-1.yml.witness.yml --witness.yaml.validate graves-cpa/count_up_down-1.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/count_up_down-1.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: y == (2U) || y == (76U) || y == (90U) || y == (121U) || y == (16U) || y == (20U) || y == (120U) || y == (95U) || y == (122U) || y == (151U) || y == (182U) || y == (103U) || y == (100U) || y == (125U) || y == (126U) || y == (47U) || y == (192U) || y == (1U) || y == (194U) || y == (167U) || y == (187U) || y == (144U) || y == (65U) || y == (150U) || y == (45U) || y == (143U) || y == (134U) || y == (154U) || y == (88U) || y == (109U) || y == (69U) || y == (158U) || y == (5U) || y == (24U) || y == (11U) || y == (137U) || y == (195U) || y == (106U) || y == (123U) || y == (62U) || y == (184U) || y == (179U) || y == (43U) || y == (23U) || y == (8U) || y == (63U) || y == (26U) || y == (186U) || y == (87U) || y == (175U) || y == (72U) || y == (99U) || y == (81U) || y == (33U) || y == (15U) || y == (41U) || y == (190U) || y == (169U) || y == (34U) || y == (56U) || y == (117U) || y == (124U) || y == (111U) || y == (161U) || y == (107U) || y == (153U) || y == (4U) || y == (22U) || y == (193U) || y == (139U) || y == (113U) || y == (176U) || y == (102U) || y == (118U) || y == (58U) || y == (160U) || y == (60U) || y == (173U) || y == (170U) || y == (52U) || y == (171U) || y == (51U) || y == (96U) || y == (157U) || y == (127U) || y == (39U) || y == (50U) || y == (149U) || y == (3U) || y == (37U) || y == (19U) || y == (7U) || y == (14U) || y == (68U) || y == (92U) || y == (6U) || y == (146U) || y == (27U) || y == (12U) || y == (55U) || y == (54U) || y == (18U) || y == (75U) || y == (61U) || y == (156U) || y == (110U) || y == (114U) || y == (97U) || y == (28U) || y == (9U) || y == (108U) || y == (129U) || y == (185U) || y == (142U) || y == (178U) || y == (116U) || y == (162U) || y == (177U) || y == (105U) || y == (30U) || y == (166U) || y == (174U) || y == (181U) || y == (66U) || y == (46U) || y == (112U) || y == (104U) || y == (32U) || y == (71U) || y == (98U) || y == (135U) || y == (57U) || y == (59U) || y == (42U) || y == (74U) || y == (94U) || y == (29U) || y == (77U) || y == (196U) || y == (101U) || y == (78U) || y == (180U) || y == (140U) || y == (189U) || y == (91U) || y == (53U) || y == (36U) || y == (44U) || y == (147U) || y == (148U) || y == (83U) || y == (128U) || y == (10U) || y == (119U) || y == (131U) || y == (21U) || y == (159U) || y == (79U) || y == (67U) || y == (70U) || y == (0U) || (!(y == (0U)) && y == (141U)) || (!(y == (0U)) && y == (93U)) || (!(y == (0U)) && y == (136U)) || (!(y == (0U)) && y == (138U)) || (!(y == (0U)) && y == (191U)) || (!(y == (0U)) && y == (163U)) || (!(y == (0U)) && y == (25U)) || (!(y == (0U)) && y == (80U)) || (!(y == (0U)) && y == (132U)) || (!(y == (0U)) && y == (40U)) || (!(y == (0U)) && y == (35U)) || (!(y == (0U)) && y == (130U)) || (!(y == (0U)) && y == (188U)) || (!(y == (0U)) && y == (89U)) || (!(y == (0U)) && y == (85U)) || (!(y == (0U)) && y == (73U)) || (!(y == (0U)) && y == (13U)) || (!(y == (0U)) && y == (133U)) || (!(y == (0U)) && y == (115U)) || (!(y == (0U)) && y == (183U)) || (!(y == (0U)) && y == (82U)) || (!(y == (0U)) && y == (86U)) || (!(y == (0U)) && y == (84U)) || (!(y == (0U)) && y == (168U)) || (!(y == (0U)) && y == (48U)) || (!(y == (0U)) && y == (155U)) || (!(y == (0U)) && y == (49U)) || (!(y == (0U)) && y == (172U)) || (!(y == (0U)) && y == (31U)) || (!(y == (0U)) && y == (145U)) || (!(y == (0U)) && y == (165U)) || (!(y == (0U)) && y == (38U)) || (!(y == (0U)) && y == (164U)) || (!(y == (0U)) && y == (64U)) || (!(y == (0U)) && y == (152U)) || (!(y == (0U)) && y == (17U)) (../plain/count_up_down-1.c:22:3)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((y == 2U || y == 76U) || y == 90U) || y == 121U) || y == 16U) || y == 20U) || y == 120U) || y == 95U) || y == 122U) || y == 151U) || y == 182U) || y == 103U) || y == 100U) || y == 125U) || y == 126U) || y == 47U) || y == 192U) || y == 1U) || y == 194U) || y == 167U) || y == 187U) || y == 144U) || y == 65U) || y == 150U) || y == 45U) || y == 143U) || y == 134U) || y == 154U) || y == 88U) || y == 109U) || y == 69U) || y == 158U) || y == 5U) || y == 24U) || y == 11U) || y == 137U) || y == 195U) || y == 106U) || y == 123U) || y == 62U) || y == 184U) || y == 179U) || y == 43U) || y == 23U) || y == 8U) || y == 63U) || y == 26U) || y == 186U) || y == 87U) || y == 175U) || y == 72U) || y == 99U) || y == 81U) || y == 33U) || y == 15U) || y == 41U) || y == 190U) || y == 169U) || y == 34U) || y == 56U) || y == 117U) || y == 124U) || y == 111U) || y == 161U) || y == 107U) || y == 153U) || y == 4U) || y == 22U) || y == 193U) || y == 139U) || y == 113U) || y == 176U) || y == 102U) || y == 118U) || y == 58U) || y == 160U) || y == 60U) || y == 173U) || y == 170U) || y == 52U) || y == 171U) || y == 51U) || y == 96U) || y == 157U) || y == 127U) || y == 39U) || y == 50U) || y == 149U) || y == 3U) || y == 37U) || y == 19U) || y == 7U) || y == 14U) || y == 68U) || y == 92U) || y == 6U) || y == 146U) || y == 27U) || y == 12U) || y == 55U) || y == 54U) || y == 18U) || y == 75U) || y == 61U) || y == 156U) || y == 110U) || y == 114U) || y == 97U) || y == 28U) || y == 9U) || y == 108U) || y == 129U) || y == 185U) || y == 142U) || y == 178U) || y == 116U) || y == 162U) || y == 177U) || y == 105U) || y == 30U) || y == 166U) || y == 174U) || y == 181U) || y == 66U) || y == 46U) || y == 112U) || y == 104U) || y == 32U) || y == 71U) || y == 98U) || y == 135U) || y == 57U) || y == 59U) || y == 42U) || y == 74U) || y == 94U) || y == 29U) || y == 77U) || y == 196U) || y == 101U) || y == 78U) || y == 180U) || y == 140U) || y == 189U) || y == 91U) || y == 53U) || y == 36U) || y == 44U) || y == 147U) || y == 148U) || y == 83U) || y == 128U) || y == 10U) || y == 119U) || y == 131U) || y == 21U) || y == 159U) || y == 79U) || y == 67U) || y == 70U) || y == 0U) || (! (y == 0U) && y == 141U)) || (! (y == 0U) && y == 93U)) || (! (y == 0U) && y == 136U)) || (! (y == 0U) && y == 138U)) || (! (y == 0U) && y == 191U)) || (! (y == 0U) && y == 163U)) || (! (y == 0U) && y == 25U)) || (! (y == 0U) && y == 80U)) || (! (y == 0U) && y == 132U)) || (! (y == 0U) && y == 40U)) || (! (y == 0U) && y == 35U)) || (! (y == 0U) && y == 130U)) || (! (y == 0U) && y == 188U)) || (! (y == 0U) && y == 89U)) || (! (y == 0U) && y == 85U)) || (! (y == 0U) && y == 73U)) || (! (y == 0U) && y == 13U)) || (! (y == 0U) && y == 133U)) || (! (y == 0U) && y == 115U)) || (! (y == 0U) && y == 183U)) || (! (y == 0U) && y == 82U)) || (! (y == 0U) && y == 86U)) || (! (y == 0U) && y == 84U)) || (! (y == 0U) && y == 168U)) || (! (y == 0U) && y == 48U)) || (! (y == 0U) && y == 155U)) || (! (y == 0U) && y == 49U)) || (! (y == 0U) && y == 172U)) || (! (y == 0U) && y == 31U)) || (! (y == 0U) && y == 145U)) || (! (y == 0U) && y == 165U)) || (! (y == 0U) && y == 38U)) || (! (y == 0U) && y == 164U)) || (! (y == 0U) && y == 64U)) || (! (y == 0U) && y == 152U)) || (! (y == 0U) && y == 17U) (../plain/count_up_down-1.c:16:21-16:24)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/count_up_down-1.c:20:5-20:8)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((y == 2U || y == 76U) || y == 90U) || y == 121U) || y == 16U) || y == 20U) || y == 120U) || y == 95U) || y == 122U) || y == 151U) || y == 182U) || y == 103U) || y == 100U) || y == 125U) || y == 126U) || y == 47U) || y == 192U) || y == 1U) || y == 194U) || y == 167U) || y == 187U) || y == 144U) || y == 65U) || y == 150U) || y == 45U) || y == 143U) || y == 134U) || y == 154U) || y == 88U) || y == 109U) || y == 69U) || y == 158U) || y == 5U) || y == 24U) || y == 11U) || y == 137U) || y == 195U) || y == 106U) || y == 123U) || y == 62U) || y == 184U) || y == 179U) || y == 43U) || y == 23U) || y == 8U) || y == 63U) || y == 26U) || y == 186U) || y == 87U) || y == 175U) || y == 72U) || y == 99U) || y == 81U) || y == 33U) || y == 15U) || y == 41U) || y == 190U) || y == 169U) || y == 34U) || y == 56U) || y == 117U) || y == 124U) || y == 111U) || y == 161U) || y == 107U) || y == 153U) || y == 4U) || y == 22U) || y == 193U) || y == 139U) || y == 113U) || y == 176U) || y == 102U) || y == 118U) || y == 58U) || y == 160U) || y == 60U) || y == 173U) || y == 170U) || y == 52U) || y == 171U) || y == 51U) || y == 96U) || y == 157U) || y == 127U) || y == 39U) || y == 50U) || y == 149U) || y == 3U) || y == 37U) || y == 19U) || y == 7U) || y == 14U) || y == 68U) || y == 92U) || y == 6U) || y == 146U) || y == 27U) || y == 12U) || y == 55U) || y == 54U) || y == 18U) || y == 75U) || y == 61U) || y == 156U) || y == 110U) || y == 114U) || y == 97U) || y == 28U) || y == 9U) || y == 108U) || y == 129U) || y == 185U) || y == 142U) || y == 178U) || y == 116U) || y == 162U) || y == 177U) || y == 105U) || y == 30U) || y == 166U) || y == 174U) || y == 181U) || y == 66U) || y == 46U) || y == 112U) || y == 104U) || y == 32U) || y == 71U) || y == 98U) || y == 135U) || y == 57U) || y == 59U) || y == 42U) || y == 74U) || y == 94U) || y == 29U) || y == 77U) || y == 196U) || y == 101U) || y == 78U) || y == 180U) || y == 140U) || y == 189U) || y == 91U) || y == 53U) || y == 36U) || y == 44U) || y == 147U) || y == 148U) || y == 83U) || y == 128U) || y == 10U) || y == 119U) || y == 131U) || y == 21U) || y == 159U) || y == 79U) || y == 67U) || y == 70U) || y == 0U) || (! (y == 0U) && y == 141U)) || (! (y == 0U) && y == 93U)) || (! (y == 0U) && y == 136U)) || (! (y == 0U) && y == 138U)) || (! (y == 0U) && y == 191U)) || (! (y == 0U) && y == 163U)) || (! (y == 0U) && y == 25U)) || (! (y == 0U) && y == 80U)) || (! (y == 0U) && y == 132U)) || (! (y == 0U) && y == 40U)) || (! (y == 0U) && y == 35U)) || (! (y == 0U) && y == 130U)) || (! (y == 0U) && y == 188U)) || (! (y == 0U) && y == 89U)) || (! (y == 0U) && y == 85U)) || (! (y == 0U) && y == 73U)) || (! (y == 0U) && y == 13U)) || (! (y == 0U) && y == 133U)) || (! (y == 0U) && y == 115U)) || (! (y == 0U) && y == 183U)) || (! (y == 0U) && y == 82U)) || (! (y == 0U) && y == 86U)) || (! (y == 0U) && y == 84U)) || (! (y == 0U) && y == 168U)) || (! (y == 0U) && y == 48U)) || (! (y == 0U) && y == 155U)) || (! (y == 0U) && y == 49U)) || (! (y == 0U) && y == 172U)) || (! (y == 0U) && y == 31U)) || (! (y == 0U) && y == 145U)) || (! (y == 0U) && y == 165U)) || (! (y == 0U) && y == 38U)) || (! (y == 0U) && y == 164U)) || (! (y == 0U) && y == 64U)) || (! (y == 0U) && y == 152U)) || (! (y == 0U) && y == 17U) (../plain/count_up_down-1.c:20:5-20:8)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 14
  dead: 0
  total lines: 14
[Warning][Witness] invariant unconfirmed: y == (2U) || y == (76U) || y == (90U) || y == (121U) || y == (16U) || y == (20U) || y == (120U) || y == (95U) || y == (122U) || y == (151U) || y == (182U) || y == (103U) || y == (100U) || y == (125U) || y == (126U) || y == (47U) || y == (192U) || y == (1U) || y == (194U) || y == (167U) || y == (187U) || y == (144U) || y == (65U) || y == (150U) || y == (45U) || y == (143U) || y == (134U) || y == (154U) || y == (88U) || y == (109U) || y == (69U) || y == (158U) || y == (5U) || y == (24U) || y == (11U) || y == (137U) || y == (195U) || y == (106U) || y == (123U) || y == (62U) || y == (184U) || y == (179U) || y == (43U) || y == (23U) || y == (8U) || y == (63U) || y == (26U) || y == (186U) || y == (87U) || y == (175U) || y == (72U) || y == (99U) || y == (81U) || y == (33U) || y == (15U) || y == (41U) || y == (190U) || y == (169U) || y == (34U) || y == (56U) || y == (117U) || y == (124U) || y == (111U) || y == (161U) || y == (107U) || y == (153U) || y == (4U) || y == (22U) || y == (193U) || y == (139U) || y == (113U) || y == (176U) || y == (102U) || y == (118U) || y == (58U) || y == (160U) || y == (60U) || y == (173U) || y == (170U) || y == (52U) || y == (171U) || y == (51U) || y == (96U) || y == (157U) || y == (127U) || y == (39U) || y == (50U) || y == (149U) || y == (3U) || y == (37U) || y == (19U) || y == (7U) || y == (14U) || y == (68U) || y == (92U) || y == (6U) || y == (146U) || y == (27U) || y == (12U) || y == (55U) || y == (54U) || y == (18U) || y == (75U) || y == (61U) || y == (156U) || y == (110U) || y == (114U) || y == (97U) || y == (28U) || y == (9U) || y == (108U) || y == (129U) || y == (185U) || y == (142U) || y == (178U) || y == (116U) || y == (162U) || y == (177U) || y == (105U) || y == (30U) || y == (166U) || y == (174U) || y == (181U) || y == (66U) || y == (46U) || y == (112U) || y == (104U) || y == (32U) || y == (71U) || y == (98U) || y == (135U) || y == (57U) || y == (59U) || y == (42U) || y == (74U) || y == (94U) || y == (29U) || y == (77U) || y == (196U) || y == (101U) || y == (78U) || y == (180U) || y == (140U) || y == (189U) || y == (91U) || y == (53U) || y == (36U) || y == (44U) || y == (147U) || y == (148U) || y == (83U) || y == (128U) || y == (10U) || y == (119U) || y == (131U) || y == (21U) || y == (159U) || y == (79U) || y == (67U) || y == (70U) || y == (0U) || (!(y == (0U)) && y == (141U)) || (!(y == (0U)) && y == (93U)) || (!(y == (0U)) && y == (136U)) || (!(y == (0U)) && y == (138U)) || (!(y == (0U)) && y == (191U)) || (!(y == (0U)) && y == (163U)) || (!(y == (0U)) && y == (25U)) || (!(y == (0U)) && y == (80U)) || (!(y == (0U)) && y == (132U)) || (!(y == (0U)) && y == (40U)) || (!(y == (0U)) && y == (35U)) || (!(y == (0U)) && y == (130U)) || (!(y == (0U)) && y == (188U)) || (!(y == (0U)) && y == (89U)) || (!(y == (0U)) && y == (85U)) || (!(y == (0U)) && y == (73U)) || (!(y == (0U)) && y == (13U)) || (!(y == (0U)) && y == (133U)) || (!(y == (0U)) && y == (115U)) || (!(y == (0U)) && y == (183U)) || (!(y == (0U)) && y == (82U)) || (!(y == (0U)) && y == (86U)) || (!(y == (0U)) && y == (84U)) || (!(y == (0U)) && y == (168U)) || (!(y == (0U)) && y == (48U)) || (!(y == (0U)) && y == (155U)) || (!(y == (0U)) && y == (49U)) || (!(y == (0U)) && y == (172U)) || (!(y == (0U)) && y == (31U)) || (!(y == (0U)) && y == (145U)) || (!(y == (0U)) && y == (165U)) || (!(y == (0U)) && y == (38U)) || (!(y == (0U)) && y == (164U)) || (!(y == (0U)) && y == (64U)) || (!(y == (0U)) && y == (152U)) || (!(y == (0U)) && y == (17U)) (../plain/count_up_down-1.c:17:3)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 1
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 2
SV-COMP result: unknown

vars = 28    evals = 35    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                            3.584s     3.598s    898.01MB      1×
  preprocess                         0.026s     0.025s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.05MB      4×
  Cabs2cil                           0.006s     0.006s      4.65MB      4×
  mergeCIL                           0.003s     0.003s      3.33MB      1×
  analysis                           3.539s     3.552s    881.04MB      1×
    createCFG                          0.001s     0.001s      0.59MB      1×
      handle                             0.001s     0.001s      0.08MB     33×
      iter_connect                       0.001s     0.001s      0.40MB     33×
        computeSCCs                        0.001s     0.001s      0.23MB     34×
    FrontC                             0.002s     0.002s      1.36MB      2×
    Cabs2cil                           0.002s     0.002s      1.43MB      2×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            0.463s     0.464s    673.80MB      1×
      S.Dom.equal                        0.001s     0.001s      0.02MB     36×
      base unassume                      0.288s     0.288s    634.34MB     11×
      cheap_full_reach                   0.001s     0.001s      0.02MB      1×
      postsolver                         0.006s     0.007s      5.76MB      1×
        postsolver_iter                    0.006s     0.007s      5.73MB      1×
    warn_global                        0.001s     0.001s      0.05MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
