/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/ps6-ll.yml.witness.yml --witness.yaml.validate cbmc/ps6-ll.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/ps6-ll.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: c == (1LL) || c == (2LL) || c == (3LL) || c == (4LL) || c == (5LL) || c == (6LL) || c == (7LL) || c == (8LL) || c == (9LL) || c == (10LL) || c == (11LL) || c == (12LL) || c == (13LL) || c == (14LL) || c == (15LL) || c == (16LL) || c == (17LL) || c == (18LL) || c == (19LL) || c == (20LL) || c == (21LL) || c == (22LL) || c == (23LL) || c == (24LL) || c == (25LL) || c == (26LL) || c == (27LL) || c == (28LL) || c == (29LL) || c == (30LL) || c == (31LL) || c == (32LL) || c == (33LL) || c == (34LL) || c == (35LL) || c == (36LL) || c == (37LL) || c == (38LL) || c == (39LL) || c == (40LL) || c == (41LL) || c == (42LL) || c == (43LL) || c == (44LL) || c == (45LL) || c == (46LL) || c == (47LL) || c == (48LL) || c == (49LL) || c == (50LL) || c == (51LL) || c == (52LL) || c == (53LL) || c == (54LL) || c == (55LL) || c == (56LL) || c == (57LL) || c == (58LL) || c == (59LL) || c == (60LL) || c == (61LL) || c == (62LL) || c == (63LL) || c == (64LL) || c == (65LL) || c == (66LL) || c == (67LL) || c == (68LL) || c == (69LL) || c == (70LL) || c == (71LL) || c == (72LL) || c == (73LL) || c == (74LL) || c == (75LL) || c == (76LL) || c == (77LL) || c == (78LL) || c == (79LL) || c == (80LL) || c == (81LL) || c == (82LL) || c == (83LL) || c == (84LL) || c == (85LL) || c == (86LL) || c == (87LL) || c == (88LL) || c == (89LL) || c == (90LL) || c == (91LL) || c == (92LL) || c == (93LL) || c == (94LL) || c == (95LL) || c == (96LL) || c == (97LL) || c == (98LL) || c == (99LL) || c == (100LL) || c == (101LL) || c == (102LL) || c == (103LL) || c == (104LL) || c == (105LL) || c == (106LL) || c == (107LL) || c == (108LL) || c == (109LL) || c == (110LL) || c == (111LL) || c == (112LL) || c == (113LL) || c == (114LL) || c == (115LL) || c == (116LL) || c == (117LL) || c == (118LL) || c == (119LL) || c == (120LL) || c == (121LL) || c == (122LL) || c == (123LL) || c == (124LL) || c == (125LL) || c == (126LL) || c == (127LL) || c == (128LL) || c == (129LL) || c == (130LL) || c == (131LL) || c == (132LL) || c == (133LL) || c == (134LL) || c == (135LL) || c == (136LL) || c == (137LL) || c == (138LL) || c == (139LL) || c == (140LL) || c == (141LL) || c == (142LL) || c == (143LL) || c == (144LL) || c == (145LL) || c == (146LL) || c == (147LL) || c == (148LL) || c == (149LL) || c == (150LL) || c == (151LL) || c == (152LL) || c == (153LL) || c == (154LL) || c == (155LL) || c == (156LL) || c == (157LL) || c == (158LL) || c == (159LL) || c == (160LL) || c == (161LL) || c == (162LL) || c == (163LL) || c == (164LL) || c == (165LL) || c == (166LL) || c == (167LL) || c == (168LL) || c == (169LL) || c == (170LL) || c == (171LL) || c == (172LL) || c == (173LL) || c == (174LL) || c == (175LL) || c == (176LL) || c == (177LL) || c == (178LL) || c == (179LL) || c == (180LL) || c == (181LL) || c == (182LL) || c == (183LL) || c == (184LL) || c == (185LL) || c == (186LL) || c == (187LL) || c == (188LL) || c == (189LL) || c == (190LL) || c == (191LL) || c == (192LL) || c == (193LL) || c == (194LL) || c == (195LL) || c == (196LL) || c == (197LL) || c == (198LL) || c == (199LL) || c == (200LL) || c == (201LL) || c == (202LL) || c == (203LL) || c == (204LL) || c == (205LL) || c == (206LL) || c == (207LL) || c == (208LL) || c == (209LL) || c == (210LL) || c == (211LL) || c == (212LL) || c == (213LL) || c == (214LL) || c == (215LL) || c == (216LL) || c == (217LL) || c == (218LL) || c == (219LL) || c == (220LL) || c == (221LL) || c == (222LL) || c == (223LL) || c == (224LL) || c == (225LL) || c == (226LL) || c == (227LL) || c == (228LL) || c == (229LL) || c == (230LL) || c == (231LL) || c == (232LL) || c == (233LL) || c == (234LL) || c == (235LL) || c == (236LL) || c == (237LL) || c == (238LL) || c == (239LL) || c == (240LL) || c == (241LL) || c == (242LL) || c == (243LL) || c == (244LL) || c == (245LL) || c == (246LL) || c == (247LL) || c == (248LL) || c == (249LL) || c == (250LL) || c == (251LL) || c == (252LL) || c == (253LL) || c == (254LL) || c == (255LL) || c == (256LL) || c == (257LL) || c == (258LL) || c == (259LL) || c == (260LL) || c == (261LL) || c == (262LL) || c == (263LL) || c == (264LL) || c == (265LL) || c == (266LL) || c == (267LL) || c == (268LL) || c == (269LL) || c == (270LL) || c == (271LL) || c == (272LL) || c == (273LL) || c == (274LL) || c == (275LL) || c == (276LL) || c == (277LL) || c == (278LL) || c == (279LL) || c == (280LL) || c == (281LL) || c == (282LL) || c == (283LL) || c == (284LL) || c == (285LL) || c == (286LL) || c == (287LL) || c == (288LL) || c == (289LL) || c == (290LL) || c == (291LL) || c == (292LL) || c == (293LL) || c == (294LL) || c == (295LL) || c == (296LL) || c == (297LL) || c == (298LL) || c == (299LL) || c == (300LL) || c == (301LL) || c == (302LL) || c == (303LL) || c == (304LL) || c == (305LL) || c == (306LL) || c == (307LL) || c == (308LL) || c == (309LL) || c == (310LL) || c == (311LL) || c == (312LL) || c == (313LL) || c == (314LL) || c == (315LL) || c == (316LL) || c == (317LL) || c == (318LL) || c == (319LL) || c == (320LL) || c == (321LL) || c == (322LL) || c == (323LL) || c == (324LL) || c == (325LL) || c == (326LL) || c == (327LL) || c == (328LL) || c == (329LL) || c == (330LL) || c == (331LL) || c == (332LL) || c == (333LL) || c == (334LL) || c == (335LL) || c == (336LL) || c == (337LL) || c == (338LL) || c == (339LL) || c == (340LL) || c == (341LL) || c == (342LL) || c == (343LL) || c == (344LL) || c == (345LL) || c == (346LL) || c == (347LL) || c == (348LL) || c == (349LL) || c == (350LL) || c == (351LL) || c == (352LL) || c == (353LL) || c == (354LL) || c == (355LL) || c == (356LL) || c == (357LL) || c == (358LL) || c == (359LL) || c == (360LL) || c == (361LL) || c == (362LL) || c == (363LL) || c == (364LL) || c == (365LL) || c == (366LL) || c == (367LL) || c == (368LL) || c == (369LL) || c == (370LL) || c == (371LL) || c == (372LL) || c == (373LL) || c == (374LL) || c == (375LL) || c == (376LL) || c == (377LL) || c == (378LL) || c == (379LL) || c == (380LL) || c == (381LL) || c == (382LL) || c == (383LL) || c == (384LL) || c == (385LL) || c == (386LL) || c == (387LL) || c == (388LL) || c == (389LL) || c == (390LL) || c == (391LL) || c == (392LL) || c == (393LL) || c == (394LL) || c == (395LL) || c == (396LL) || c == (397LL) || c == (398LL) || c == (399LL) || c == (400LL) (../plain/ps6-ll.c:34:9)
[Warning][Witness] couldn't locate invariant: y == (1LL) || y == (2LL) || y == (3LL) || y == (4LL) || y == (5LL) || y == (6LL) || y == (7LL) || y == (8LL) || y == (9LL) || y == (10LL) || y == (11LL) || y == (12LL) || y == (13LL) || y == (14LL) || y == (15LL) || y == (16LL) || y == (17LL) || y == (18LL) || y == (19LL) || y == (20LL) || y == (21LL) || y == (22LL) || y == (23LL) || y == (24LL) || y == (25LL) || y == (26LL) || y == (27LL) || y == (28LL) || y == (29LL) || y == (30LL) || y == (31LL) || y == (32LL) || y == (33LL) || y == (34LL) || y == (35LL) || y == (36LL) || y == (37LL) || y == (38LL) || y == (39LL) || y == (40LL) || y == (41LL) || y == (42LL) || y == (43LL) || y == (44LL) || y == (45LL) || y == (46LL) || y == (47LL) || y == (48LL) || y == (49LL) || y == (50LL) || y == (51LL) || y == (52LL) || y == (53LL) || y == (54LL) || y == (55LL) || y == (56LL) || y == (57LL) || y == (58LL) || y == (59LL) || y == (60LL) || y == (61LL) || y == (62LL) || y == (63LL) || y == (64LL) || y == (65LL) || y == (66LL) || y == (67LL) || y == (68LL) || y == (69LL) || y == (70LL) || y == (71LL) || y == (72LL) || y == (73LL) || y == (74LL) || y == (75LL) || y == (76LL) || y == (77LL) || y == (78LL) || y == (79LL) || y == (80LL) || y == (81LL) || y == (82LL) || y == (83LL) || y == (84LL) || y == (85LL) || y == (86LL) || y == (87LL) || y == (88LL) || y == (89LL) || y == (90LL) || y == (91LL) || y == (92LL) || y == (93LL) || y == (94LL) || y == (95LL) || y == (96LL) || y == (97LL) || y == (98LL) || y == (99LL) || y == (100LL) || y == (101LL) || y == (102LL) || y == (103LL) || y == (104LL) || y == (105LL) || y == (106LL) || y == (107LL) || y == (108LL) || y == (109LL) || y == (110LL) || y == (111LL) || y == (112LL) || y == (113LL) || y == (114LL) || y == (115LL) || y == (116LL) || y == (117LL) || y == (118LL) || y == (119LL) || y == (120LL) || y == (121LL) || y == (122LL) || y == (123LL) || y == (124LL) || y == (125LL) || y == (126LL) || y == (127LL) || y == (128LL) || y == (129LL) || y == (130LL) || y == (131LL) || y == (132LL) || y == (133LL) || y == (134LL) || y == (135LL) || y == (136LL) || y == (137LL) || y == (138LL) || y == (139LL) || y == (140LL) || y == (141LL) || y == (142LL) || y == (143LL) || y == (144LL) || y == (145LL) || y == (146LL) || y == (147LL) || y == (148LL) || y == (149LL) || y == (150LL) || y == (151LL) || y == (152LL) || y == (153LL) || y == (154LL) || y == (155LL) || y == (156LL) || y == (157LL) || y == (158LL) || y == (159LL) || y == (160LL) || y == (161LL) || y == (162LL) || y == (163LL) || y == (164LL) || y == (165LL) || y == (166LL) || y == (167LL) || y == (168LL) || y == (169LL) || y == (170LL) || y == (171LL) || y == (172LL) || y == (173LL) || y == (174LL) || y == (175LL) || y == (176LL) || y == (177LL) || y == (178LL) || y == (179LL) || y == (180LL) || y == (181LL) || y == (182LL) || y == (183LL) || y == (184LL) || y == (185LL) || y == (186LL) || y == (187LL) || y == (188LL) || y == (189LL) || y == (190LL) || y == (191LL) || y == (192LL) || y == (193LL) || y == (194LL) || y == (195LL) || y == (196LL) || y == (197LL) || y == (198LL) || y == (199LL) || y == (200LL) || y == (201LL) || y == (202LL) || y == (203LL) || y == (204LL) || y == (205LL) || y == (206LL) || y == (207LL) || y == (208LL) || y == (209LL) || y == (210LL) || y == (211LL) || y == (212LL) || y == (213LL) || y == (214LL) || y == (215LL) || y == (216LL) || y == (217LL) || y == (218LL) || y == (219LL) || y == (220LL) || y == (221LL) || y == (222LL) || y == (223LL) || y == (224LL) || y == (225LL) || y == (226LL) || y == (227LL) || y == (228LL) || y == (229LL) || y == (230LL) || y == (231LL) || y == (232LL) || y == (233LL) || y == (234LL) || y == (235LL) || y == (236LL) || y == (237LL) || y == (238LL) || y == (239LL) || y == (240LL) || y == (241LL) || y == (242LL) || y == (243LL) || y == (244LL) || y == (245LL) || y == (246LL) || y == (247LL) || y == (248LL) || y == (249LL) || y == (250LL) || y == (251LL) || y == (252LL) || y == (253LL) || y == (254LL) || y == (255LL) || y == (256LL) || y == (257LL) || y == (258LL) || y == (259LL) || y == (260LL) || y == (261LL) || y == (262LL) || y == (263LL) || y == (264LL) || y == (265LL) || y == (266LL) || y == (267LL) || y == (268LL) || y == (269LL) || y == (270LL) || y == (271LL) || y == (272LL) || y == (273LL) || y == (274LL) || y == (275LL) || y == (276LL) || y == (277LL) || y == (278LL) || y == (279LL) || y == (280LL) || y == (281LL) || y == (282LL) || y == (283LL) || y == (284LL) || y == (285LL) || y == (286LL) || y == (287LL) || y == (288LL) || y == (289LL) || y == (290LL) || y == (291LL) || y == (292LL) || y == (293LL) || y == (294LL) || y == (295LL) || y == (296LL) || y == (297LL) || y == (298LL) || y == (299LL) || y == (300LL) || y == (301LL) || y == (302LL) || y == (303LL) || y == (304LL) || y == (305LL) || y == (306LL) || y == (307LL) || y == (308LL) || y == (309LL) || y == (310LL) || y == (311LL) || y == (312LL) || y == (313LL) || y == (314LL) || y == (315LL) || y == (316LL) || y == (317LL) || y == (318LL) || y == (319LL) || y == (320LL) || y == (321LL) || y == (322LL) || y == (323LL) || y == (324LL) || y == (325LL) || y == (326LL) || y == (327LL) || y == (328LL) || y == (329LL) || y == (330LL) || y == (331LL) || y == (332LL) || y == (333LL) || y == (334LL) || y == (335LL) || y == (336LL) || y == (337LL) || y == (338LL) || y == (339LL) || y == (340LL) || y == (341LL) || y == (342LL) || y == (343LL) || y == (344LL) || y == (345LL) || y == (346LL) || y == (347LL) || y == (348LL) || y == (349LL) || y == (350LL) || y == (351LL) || y == (352LL) || y == (353LL) || y == (354LL) || y == (355LL) || y == (356LL) || y == (357LL) || y == (358LL) || y == (359LL) || y == (360LL) || y == (361LL) || y == (362LL) || y == (363LL) || y == (364LL) || y == (365LL) || y == (366LL) || y == (367LL) || y == (368LL) || y == (369LL) || y == (370LL) || y == (371LL) || y == (372LL) || y == (373LL) || y == (374LL) || y == (375LL) || y == (376LL) || y == (377LL) || y == (378LL) || y == (379LL) || y == (380LL) || y == (381LL) || y == (382LL) || y == (383LL) || y == (384LL) || y == (385LL) || y == (386LL) || y == (387LL) || y == (388LL) || y == (389LL) || y == (390LL) || y == (391LL) || y == (392LL) || y == (393LL) || y == (394LL) || y == (395LL) || y == (396LL) || y == (397LL) || y == (398LL) || y == (399LL) || y == (400LL) (../plain/ps6-ll.c:35:9)

runtime: 00:00:10.089
vars: 44, evals: 3496

|rho|=44
|called|=5
|stable|=43
|infl|=42
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=32
Found 6 contexts for 5 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_assert (2009) on ../plain/ps6-ll.c:9:1-15:1
1	contexts for entry state of main (2012) on ../plain/ps6-ll.c:17:1-41:1
1	contexts for entry state of __VERIFIER_nondet_short (344) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:33:64-33:121
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/ps6-ll.c:6:1-8:1
1	contexts for entry state of reach_error (1999) on ../plain/ps6-ll.c:3:1-3:72

Memory statistics: total=1770.44MB, max=14.22MB, minor=1767.43MB, major=29.37MB, promoted=26.35MB
    minor collections=847  major collections=10 compactions=0

[Info][Witness] unassume invariant: (x == 0LL && y == 0LL) && c == 0LL (../plain/ps6-ll.c:25:5-25:10)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (../plain/ps6-ll.c:28:9-28:90)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/ps6-ll.c:28:9-28:90)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/ps6-ll.c:34:9-34:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/ps6-ll.c:35:9-35:34)
[Info][Witness] unassume invariant: (x == 0LL && y == 0LL) && c == 0LL (../plain/ps6-ll.c:35:9-35:34)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (../plain/ps6-ll.c:38:5-38:86)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/ps6-ll.c:38:5-38:86)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/ps6-ll.c:39:5-39:34)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/ps6-ll.c:39:5-39:34)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 24
  dead: 0
  total lines: 24
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/ps6-ll.c:27:12-27:13)
[Warning][Witness] invariant unconfirmed: c == (0LL) (../plain/ps6-ll.c:27:5)
[Warning][Witness] invariant unconfirmed: y == (0LL) (../plain/ps6-ll.c:24:5)
[Warning][Witness] invariant unconfirmed: x == (0LL) (../plain/ps6-ll.c:25:5)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 3
  refuted: 0
  error: 2
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 5
SV-COMP result: unknown

vars = 44    evals = 4539    narrow_reuses = 128

Timings:
                                  cputime   walltime   allocated   count
Default                           18.499s    18.501s   2312.44MB      1×
  preprocess                         0.024s     0.023s      0.01MB      1×
  FrontC                             0.004s     0.004s      4.14MB      4×
  Cabs2cil                           0.005s     0.005s      4.85MB      4×
  mergeCIL                           0.003s     0.003s      3.34MB      1×
  analysis                          18.459s    18.460s   2295.15MB      1×
    createCFG                          0.001s     0.001s      0.62MB      1×
      handle                             0.001s     0.001s      0.09MB     34×
      iter_connect                       0.001s     0.001s      0.42MB     34×
        computeSCCs                        0.001s     0.001s      0.24MB     35×
    FrontC                             0.001s     0.001s      0.04MB      6×
    Cabs2cil                           0.005s     0.005s      0.58MB      6×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                           18.439s    18.440s   2283.75MB      1×
      S.Dom.equal                        0.009s     0.018s      1.57MB   4667×
      base unassume                      0.226s     0.228s    126.52MB   1035×
      cheap_full_reach                   0.001s     0.001s      0.02MB      1×
      postsolver                         0.127s     0.127s      9.21MB      1×
        postsolver_iter                    0.126s     0.126s      9.17MB      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×
