/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/afnp2014.yml.witness.yml --witness.yaml.validate cbmc/afnp2014.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/afnp2014.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 == (1) || x == (2) || x == (7) || x == (11) || x == (16) || x == (29) || x == (37) || x == (46) || x == (67) || x == (79) || x == (92) || x == (121) || x == (137) || x == (154) || x == (191) || x == (211) || x == (232) || x == (277) || x == (301) || x == (326) || x == (379) || x == (407) || x == (436) || x == (497) || x == (529) || x == (562) || x == (631) || x == (667) || x == (704) || x == (781) || x == (821) || x == (862) || x == (947) || x == (991) || x == (1036) || x == (1129) || x == (1177) || x == (1226) || x == (1327) || x == (1379) || x == (1432) || x == (1541) || x == (1597) || x == (1654) || x == (1771) || x == (1831) || x == (1892) || x == (2017) || x == (2081) || x == (2146) || x == (2279) || x == (2347) || x == (2416) || x == (2557) || x == (2629) || x == (2702) || x == (2851) || x == (2927) || x == (3004) || x == (3161) || x == (3241) || x == (3322) || x == (3487) || x == (3571) || x == (3656) || x == (3829) || x == (3917) || x == (4006) || x == (4187) || x == (4279) || x == (4372) || x == (4561) || x == (4657) || x == (4754) || x == (4951) || x == (5051) || x == (5152) || x == (5357) || x == (5461) || x == (5566) || x == (5779) || x == (5887) || x == (5996) || x == (6217) || x == (6329) || x == (6442) || x == (6671) || x == (6787) || x == (6904) || x == (7141) || x == (7261) || x == (7382) || x == (7627) || x == (7751) || x == (7876) || x == (8129) || x == (8257) || x == (8386) || x == (8647) || x == (8779) || x == (8912) || x == (9181) || x == (9317) || x == (9454) || x == (9731) || x == (9871) || x == (10012) || x == (10297) || x == (10441) || x == (10586) || x == (10879) || x == (11027) || x == (11176) || x == (11477) || x == (11629) || x == (11782) || x == (12091) || x == (12247) || x == (12404) || x == (12721) || x == (12881) || x == (13042) || x == (13367) || x == (13531) || x == (13696) || x == (14029) || x == (14197) || x == (14366) || x == (14707) || x == (14879) || x == (15052) || x == (15401) || x == (15577) || x == (15754) || x == (16111) || x == (16291) || x == (16472) || x == (16837) || x == (17021) || x == (17206) || x == (17579) || x == (17767) || x == (17956) || x == (18337) || x == (18529) || x == (18722) || x == (19111) || x == (19307) || x == (19504) || x == (19901) || x == (20101) || x == (20302) || x == (20707) || x == (20911) || x == (21116) || x == (21529) || x == (21737) || x == (21946) || x == (22367) || x == (22579) || x == (22792) || x == (23221) || x == (23437) || x == (23654) || x == (24091) || x == (24311) || x == (24532) || x == (24977) || x == (25201) || x == (25426) || x == (25879) || x == (26107) || x == (26336) || x == (26797) || x == (27029) || x == (27262) || x == (27731) || x == (27967) || x == (28204) || x == (28681) || x == (28921) || x == (29162) || x == (29647) || x == (29891) || x == (30136) || x == (30629) || x == (30877) || x == (31126) || x == (31627) || x == (31879) || x == (32132) || x == (32641) || x == (32897) || x == (33154) || x == (33671) || x == (33931) || x == (34192) || x == (34717) || x == (34981) || x == (35246) || x == (35779) || x == (36047) || x == (36316) || x == (36857) || x == (37129) || x == (37402) || x == (37951) || x == (38227) || x == (38504) || x == (39061) || x == (39341) || x == (39622) || x == (40187) || x == (40471) || x == (40756) || x == (41329) || x == (41617) || x == (41906) || x == (42487) || x == (42779) || x == (43072) || x == (43661) || x == (43957) || x == (44254) || x == (44851) || x == (45151) || x == (45452) || x == (46057) || x == (46361) || x == (46666) || x == (47279) || x == (47587) || x == (47896) || x == (48517) || x == (48829) || x == (49142) || x == (49771) || x == (50087) || x == (50404) || x == (51041) || x == (51361) || x == (51682) || x == (52327) || x == (52651) || x == (52976) || x == (53629) || x == (53957) || x == (54286) || x == (54947) || x == (55279) || x == (55612) || x == (56281) || x == (56617) || x == (56954) || x == (57631) || x == (57971) || x == (58312) || x == (58997) || x == (59341) || x == (59686) || x == (60379) || x == (60727) || x == (61076) || x == (61777) || x == (62129) || x == (62482) || x == (63191) || x == (63547) || x == (63904) || x == (64621) || x == (64981) || x == (65342) || x == (66067) || x == (66431) || x == (66796) || x == (67529) || x == (67897) || x == (68266) || x == (69007) || x == (69379) || x == (69752) || x == (70501) || x == (70877) || x == (71254) || x == (72011) || x == (72391) || x == (72772) || x == (73537) || x == (73921) || x == (74306) || x == (75079) || x == (75467) || x == (75856) || x == (76246) || x == (76637) || x == (77422) || x == (77816) || x == (78211) || x == (79004) || x == (79402) || x == (79801) || x == (80602) || x == (81004) || x == (81407) || x == (82216) || x == (82622) || x == (83029) || x == (83846) || x == (84256) || x == (84667) || x == (85492) || x == (85906) || x == (86321) || x == (87154) || x == (87572) || x == (87991) || x == (88832) || x == (89254) || x == (89677) || x == (90526) || x == (90952) || x == (91379) || x == (92236) || x == (92666) || x == (93097) || x == (93962) || x == (94396) || x == (94831) || x == (95704) || x == (96142) || x == (96581) || x == (97021) || x == (97904) || x == (98347) || x == (98791) || x == (99682) || x == (100129) || x == (100577) || x == (101476) || x == (101927) || x == (102379) || x == (103286) || x == (103741) || x == (104197) || x == (105112) || x == (105571) || x == (106031) || x == (106492) || x == (106954) || x == (107417) || x == (108346) || x == (108812) || x == (109279) || x == (110216) || x == (110686) || x == (111157) || x == (112102) || x == (112576) || x == (113051) || x == (114004) || x == (114482) || x == (114961) || x == (115922) || x == (116404) || x == (116887) || x == (117856) || x == (118342) || x == (118829) || x == (119806) || x == (120296) || x == (120787) || x == (121772) || x == (122266) || x == (122761) || x == (123754) || x == (124252) || x == (124751) || x == (125752) || x == (126254) || x == (126757) || x == (127766) || x == (128272) || x == (128779) || x == (129287) || x == (129796) || x == (130306) || x == (131329) || x == (131842) || x == (132356) || x == (133387) || x == (133904) || x == (134422) || x == (134941) || x == (135461) || x == (135982) || x == (136504) || x == (137027) || x == (137551) || x == (138076) || x == (138602) || x == (139129) || x == (139657) || x == (140186) || x == (140716) || x == (141247) || x == (141779) || x == (142312) || x == (142846) || x == (143381) || x == (143917) || x == (144454) || x == (144992) || x == (145531) || x == (146071) || x == (146612) || x == (147154) || x == (147697) || x == (148241) || x == (148786) || x == (149332) || x == (149879) || x == (150427) || x == (150976) || x == (151526) || x == (152077) || x == (152629) || x == (153182) || x == (154291) || x == (154847) || x == (155404) || x == (155962) || x == (156521) || x == (157081) || x == (157642) || x == (158204) || x == (158767) || x == (159331) || x == (159896) || x == (160462) || x == (161029) || x == (161597) || x == (162166) || x == (162736) || x == (163307) || x == (163879) || x == (164452) || x == (165026) || x == (165601) || x == (166177) || x == (166754) || x == (167332) || x == (167911) || x == (168491) || x == (169072) || x == (169654) || x == (170237) || x == (170821) || x == (171406) || x == (171992) || x == (172579) || x == (173167) || x == (173756) || x == (174346) || x == (174937) || x == (175529) || x == (176122) || x == (176716) || x == (177311) || x == (177907) || x == (178504) || x == (179102) || x == (179701) || x == (180301) || x == (180902) || x == (181504) || x == (182107) || x == (182711) || x == (183316) || x == (183922) || x == (184529) || x == (185137) || x == (185746) || x == (186356) || x == (186967) || x == (187579) || x == (188192) || x == (188806) || x == (189421) || x == (190037) || x == (190654) || x == (191272) || x == (191891) || x == (192511) || x == (193132) || x == (193754) || x == (194377) || x == (195001) || x == (195626) || x == (196252) || x == (196879) || x == (197507) || x == (198136) || x == (198766) || x == (199397) || x == (200029) || x == (200662) || x == (201296) || x == (201931) || x == (202567) || x == (203204) || x == (203842) || x == (204481) || x == (205121) || x == (205762) || x == (206404) || x == (207047) || x == (207691) || x == (208336) || x == (208982) || x == (209629) || x == (210277) || x == (210926) || x == (211576) || x == (212227) || x == (212879) || x == (213532) || x == (214186) || x == (214841) || x == (215497) || x == (216154) || x == (216812) || x == (217471) || x == (218131) || x == (218792) || x == (219454) || x == (220117) || x == (220781) || x == (221446) || x == (222112) || x == (222779) || x == (223447) || x == (224116) || x == (224786) || x == (225457) || x == (226129) || x == (226802) || x == (227476) || x == (228151) || x == (228827) || x == (229504) || x == (230182) || x == (230861) || x == (231541) || x == (232222) || x == (232904) || x == (233587) || x == (234271) || x == (234956) || x == (235642) || x == (236329) || x == (237017) || x == (237706) || x == (238396) || x == (239087) || x == (239779) || x == (240472) || x == (241166) || x == (241861) || x == (242557) || x == (243254) || x == (243952) || x == (244651) || x == (245351) || x == (246052) || x == (246754) || x == (247457) || x == (248161) || x == (248866) || x == (249572) || x == (250279) || x == (250987) || x == (251696) || x == (252406) || x == (253117) || x == (253829) || x == (254542) || x == (255256) || x == (255971) || x == (256687) || x == (257404) || x == (258122) || x == (258841) || x == (259561) || x == (260282) || x == (261004) || x == (261727) || x == (262451) || x == (263176) || x == (263902) || x == (264629) || x == (265357) || x == (266086) || x == (266816) || x == (267547) || x == (268279) || x == (269012) || x == (269746) || x == (270481) || x == (271217) || x == (271954) || x == (272692) || x == (273431) || x == (274171) || x == (274912) || x == (275654) || x == (276397) || x == (277141) || x == (277886) || x == (278632) || x == (279379) || x == (280127) || x == (280876) || x == (281626) || x == (282377) || x == (283129) || x == (283882) || x == (284636) || x == (285391) || x == (286147) || x == (286904) || x == (287662) || x == (288421) || x == (289181) || x == (289942) || x == (290704) || x == (291467) || x == (292231) || x == (292996) || x == (293762) || x == (294529) || x == (295297) || x == (296066) || x == (296836) || x == (297607) || x == (298379) || x == (299152) || x == (299926) || x == (300701) || x == (301477) || x == (302254) || x == (303032) || x == (303811) || x == (304591) || x == (305372) || x == (306154) || x == (306937) || x == (307721) || x == (308506) || x == (309292) || x == (310079) || x == (310867) || x == (311656) || x == (312446) || x == (313237) || x == (314029) || x == (314822) || x == (315616) || x == (316411) || x == (317207) || x == (318004) || x == (318802) || x == (319601) || x == (320401) || x == (321202) || x == (322004) || x == (322807) || x == (323611) || x == (324416) || x == (325222) || x == (326029) || x == (326837) || x == (327646) || x == (328456) || x == (329267) || x == (330079) || x == (330892) || x == (331706) || x == (332521) || x == (333337) || x == (334154) || x == (334972) || x == (335791) || x == (336611) || x == (337432) || x == (338254) || x == (339077) || x == (339901) || x == (340726) || x == (341552) || x == (342379) || x == (343207) || x == (344036) || x == (344866) || x == (345697) || x == (346529) || x == (347362) || x == (348196) || x == (349031) || x == (349867) || x == (350704) || x == (351542) || x == (352381) || x == (353221) || x == (354062) || x == (354904) || x == (355747) || x == (356591) || x == (357436) || x == (358282) || x == (359129) || x == (359977) || x == (360826) || x == (361676) || x == (362527) || x == (363379) || x == (364232) || x == (365086) || x == (365941) || x == (366797) || x == (367654) || x == (368512) || x == (369371) || x == (370231) || x == (371092) || x == (371954) || x == (372817) || x == (373681) || x == (374546) || x == (375412) || x == (376279) || x == (377147) || x == (378016) || x == (378886) || x == (379757) || x == (380629) || x == (381502) || x == (382376) || x == (383251) || x == (384127) || x == (385004) || x == (385882) || x == (386761) || x == (387641) || x == (388522) || x == (389404) || x == (390287) || x == (391171) || x == (392056) || x == (392942) || x == (393829) || x == (394717) || x == (395606) || x == (396496) || x == (397387) || x == (398279) || x == (399172) || x == (400066) || x == (400961) || x == (401857) || x == (402754) || x == (403652) || x == (404551) || x == (405451) || x == (406352) || x == (407254) || x == (408157) || x == (409061) || x == (409966) || x == (410872) || x == (411779) || x == (412687) || x == (413596) || x == (414506) || x == (415417) || x == (416329) || x == (417242) || x == (418156) || x == (419071) || x == (419987) || x == (420904) || x == (421822) || x == (422741) || x == (423661) || x == (424582) || x == (425504) || x == (426427) || x == (427351) || x == (428276) || x == (429202) || x == (430129) || x == (431057) || x == (431986) || x == (432916) || x == (433847) || x == (434779) || x == (435712) || x == (436646) || x == (437581) || x == (438517) || x == (439454) || x == (440392) || x == (441331) || x == (442271) || x == (443212) || x == (444154) || x == (445097) || x == (446041) || x == (446986) || x == (447932) || x == (448879) || x == (449827) || x == (450776) || x == (451726) || x == (452677) || x == (453629) || x == (454582) || x == (455536) || x == (456491) || x == (457447) || x == (458404) || x == (459362) || x == (460321) || x == (461281) || x == (462242) || x == (463204) || x == (464167) || x == (465131) || x == (466096) || x == (467062) || x == (468029) || x == (468997) || x == (469966) || x == (470936) || x == (471907) || x == (472879) || x == (473852) || x == (474826) || x == (475801) || x == (476777) || x == (477754) || x == (478732) || x == (479711) || x == (480691) || x == (481672) || x == (482654) || x == (483637) || x == (484621) || x == (485606) || x == (486592) || x == (487579) || x == (488567) || x == (489556) || x == (490546) || x == (491537) || x == (492529) || x == (493522) || x == (494516) || x == (495511) || x == (496507) || x == (497504) || x == (498502) || x == (499501) (../plain/afnp2014.i:29:9)
[Info][Witness] unassume invariant: x == 1 && y == 0 (../plain/afnp2014.i:26:9-26:14)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/afnp2014.i:28:9-28:18)
[Info][Witness] unassume invariant: x == 1 && y == 0 (../plain/afnp2014.i:29:9-29:18)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/afnp2014.i:14:1-16:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 14
  dead: 2 (2 in uncalled functions)
  total lines: 16
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (../plain/afnp2014.i:12:73-12:74)
[Warning][Witness] invariant unconfirmed: y == (0) (../plain/afnp2014.i:27:5)
[Warning][Witness] invariant unconfirmed: x == (1) (../plain/afnp2014.i:26:5)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 2
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 3
SV-COMP result: unknown

vars = 34    evals = 67    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                            0.087s     0.098s     51.19MB      1×
  preprocess                         0.025s     0.024s      0.01MB      1×
  FrontC                             0.004s     0.004s      4.12MB      4×
  Cabs2cil                           0.006s     0.006s      4.72MB      4×
  mergeCIL                           0.003s     0.003s      3.34MB      1×
  analysis                           0.046s     0.057s     34.06MB      1×
    createCFG                          0.001s     0.001s      0.61MB      1×
      handle                             0.001s     0.001s      0.09MB     34×
      iter_connect                       0.001s     0.001s      0.41MB     34×
        computeSCCs                        0.001s     0.001s      0.24MB     35×
    FrontC                             0.001s     0.001s      0.03MB      4×
    Cabs2cil                           0.001s     0.001s      0.40MB      4×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            0.033s     0.034s     23.79MB      1×
      S.Dom.equal                        0.001s     0.001s      0.03MB     68×
      base unassume                      0.001s     0.001s      1.29MB     15×
      cheap_full_reach                   0.001s     0.001s      0.02MB      1×
      postsolver                         0.009s     0.009s      5.12MB      1×
        postsolver_iter                    0.009s     0.009s      5.08MB      1×
    warn_global                        0.001s     0.001s      0.10MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
