/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/gauss_sum.yml.witness.yml --witness.yaml.validate cbmc/gauss_sum.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/gauss_sum.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: i == (1) || i == (2) || i == (4) || i == (5) || i == (8) || i == (9) || i == (12) || i == (13) || i == (16) || i == (17) || i == (20) || i == (21) || i == (24) || i == (25) || i == (28) || i == (29) || i == (32) || i == (33) || i == (36) || i == (37) || i == (40) || i == (41) || i == (44) || i == (45) || i == (48) || i == (49) || i == (52) || i == (53) || i == (56) || i == (57) || i == (60) || i == (61) || i == (64) || i == (65) || i == (68) || i == (69) || i == (72) || i == (73) || i == (76) || i == (77) || i == (80) || i == (81) || i == (84) || i == (85) || i == (88) || i == (89) || i == (92) || i == (93) || i == (96) || i == (97) || i == (100) || i == (101) || i == (104) || i == (105) || i == (108) || i == (109) || i == (112) || i == (113) || i == (116) || i == (117) || i == (120) || i == (121) || i == (124) || i == (125) || i == (128) || i == (129) || i == (132) || i == (133) || i == (136) || i == (137) || i == (140) || i == (141) || i == (144) || i == (145) || i == (148) || i == (149) || i == (152) || i == (153) || i == (156) || i == (157) || i == (160) || i == (161) || i == (164) || i == (165) || i == (168) || i == (169) || i == (172) || i == (173) || i == (176) || i == (177) || i == (180) || i == (181) || i == (184) || i == (185) || i == (188) || i == (189) || i == (192) || i == (193) || i == (196) || i == (197) || i == (200) || i == (201) || i == (204) || i == (205) || i == (208) || i == (209) || i == (212) || i == (213) || i == (216) || i == (217) || i == (220) || i == (221) || i == (224) || i == (225) || i == (228) || i == (229) || i == (232) || i == (233) || i == (236) || i == (237) || i == (240) || i == (241) || i == (244) || i == (245) || i == (248) || i == (249) || i == (252) || i == (253) || i == (256) || i == (257) || i == (260) || i == (261) || i == (264) || i == (265) || i == (268) || i == (269) || i == (272) || i == (273) || i == (276) || i == (277) || i == (280) || i == (281) || i == (284) || i == (285) || i == (288) || i == (289) || i == (292) || i == (293) || i == (296) || i == (297) || i == (300) || i == (301) || i == (304) || i == (305) || i == (308) || i == (309) || i == (312) || i == (313) || i == (316) || i == (317) || i == (320) || i == (321) || i == (324) || i == (325) || i == (328) || i == (329) || i == (332) || i == (333) || i == (336) || i == (337) || i == (339) || i == (340) || i == (342) || i == (343) || i == (345) || i == (346) || i == (347) || i == (349) || i == (350) || i == (351) || i == (353) || i == (354) || i == (355) || i == (357) || i == (358) || i == (359) || i == (361) || i == (362) || i == (363) || i == (365) || i == (366) || i == (368) || i == (369) || i == (370) || i == (372) || i == (373) || i == (374) || i == (376) || i == (377) || i == (378) || i == (380) || i == (381) || i == (382) || i == (384) || i == (385) || i == (386) || i == (388) || i == (389) || i == (390) || i == (392) || i == (393) || i == (394) || i == (396) || i == (397) || i == (398) || i == (400) || i == (401) || i == (402) || i == (404) || i == (405) || i == (406) || i == (408) || i == (409) || i == (410) || i == (412) || i == (413) || i == (415) || i == (417) || i == (418) || i == (421) || i == (422) || i == (425) || i == (426) || i == (429) || i == (430) || i == (432) || i == (433) || i == (435) || i == (436) || i == (438) || i == (439) || i == (440) || i == (442) || i == (443) || i == (444) || i == (446) || i == (447) || i == (448) || i == (450) || i == (451) || i == (452) || i == (454) || i == (455) || i == (456) || i == (457) || i == (459) || i == (460) || i == (461) || i == (463) || i == (464) || i == (465) || i == (467) || i == (468) || i == (469) || i == (471) || i == (472) || i == (473) || i == (475) || i == (476) || i == (477) || i == (479) || i == (480) || i == (481) || i == (483) || i == (484) || i == (485) || i == (487) || i == (488) || i == (489) || i == (491) || i == (492) || i == (493) || i == (495) || i == (496) || i == (497) || i == (499) || i == (500) || i == (501) || i == (502) || i == (503) || i == (505) || i == (506) || i == (508) || i == (509) || i == (510) || i == (512) || i == (513) || i == (514) || i == (516) || i == (517) || i == (518) || i == (520) || i == (521) || i == (522) || i == (524) || i == (525) || i == (526) || i == (528) || i == (529) || i == (530) || i == (532) || i == (533) || i == (534) || i == (536) || i == (537) || i == (538) || i == (540) || i == (541) || i == (542) || i == (544) || i == (545) || i == (546) || i == (548) || i == (549) || i == (550) || i == (552) || i == (553) || i == (555) || i == (556) || i == (557) || i == (559) || i == (560) || i == (561) || i == (563) || i == (564) || i == (565) || i == (567) || i == (568) || i == (569) || i == (571) || i == (572) || i == (573) || i == (575) || i == (576) || i == (577) || i == (579) || i == (580) || i == (581) || i == (583) || i == (584) || i == (585) || i == (587) || i == (588) || i == (589) || i == (591) || i == (592) || i == (593) || i == (595) || i == (596) || i == (597) || i == (599) || i == (600) || i == (602) || i == (603) || i == (604) || i == (606) || i == (607) || i == (608) || i == (610) || i == (611) || i == (612) || i == (614) || i == (615) || i == (616) || i == (618) || i == (619) || i == (620) || i == (621) || i == (623) || i == (624) || i == (625) || i == (627) || i == (628) || i == (629) || i == (631) || i == (632) || i == (633) || i == (635) || i == (636) || i == (637) || i == (639) || i == (640) || i == (641) || i == (643) || i == (644) || i == (645) || i == (647) || i == (648) || i == (649) || i == (651) || i == (652) || i == (653) || i == (655) || i == (656) || i == (657) || i == (659) || i == (660) || i == (661) || i == (663) || i == (664) || i == (665) || i == (666) || i == (667) || i == (669) || i == (670) || i == (672) || i == (673) || i == (674) || i == (676) || i == (677) || i == (678) || i == (680) || i == (681) || i == (682) || i == (684) || i == (685) || i == (686) || i == (688) || i == (689) || i == (690) || i == (692) || i == (693) || i == (694) || i == (696) || i == (697) || i == (698) || i == (700) || i == (701) || i == (702) || i == (704) || i == (705) || i == (706) || i == (708) || i == (709) || i == (710) || i == (712) || i == (713) || i == (714) || i == (715) || i == (717) || i == (718) || i == (719) || i == (721) || i == (722) || i == (723) || i == (725) || i == (726) || i == (727) || i == (729) || i == (730) || i == (731) || i == (733) || i == (734) || i == (735) || i == (737) || i == (738) || i == (739) || i == (741) || i == (742) || i == (743) || i == (745) || i == (746) || i == (747) || i == (749) || i == (750) || i == (751) || i == (753) || i == (754) || i == (755) || i == (757) || i == (758) || i == (759) || i == (760) || i == (761) || i == (763) || i == (764) || i == (766) || i == (767) || i == (768) || i == (770) || i == (771) || i == (772) || i == (774) || i == (775) || i == (776) || i == (778) || i == (779) || i == (780) || i == (782) || i == (783) || i == (784) || i == (786) || i == (787) || i == (788) || i == (790) || i == (791) || i == (792) || i == (794) || i == (795) || i == (796) || i == (799) || i == (800) || i == (803) || i == (804) || i == (806) || i == (807) || i == (809) || i == (810) || i == (812) || i == (813) || i == (814) || i == (816) || i == (817) || i == (818) || i == (820) || i == (821) || i == (822) || i == (824) || i == (825) || i == (826) || i == (828) || i == (829) || i == (830) || i == (832) || i == (833) || i == (835) || i == (836) || i == (837) || i == (839) || i == (840) || i == (841) || i == (843) || i == (844) || i == (845) || i == (847) || i == (848) || i == (849) || i == (851) || i == (852) || i == (853) || i == (854) || i == (856) || i == (857) || i == (858) || i == (860) || i == (861) || i == (862) || i == (864) || i == (865) || i == (866) || i == (868) || i == (869) || i == (870) || i == (872) || i == (873) || i == (874) || i == (876) || i == (877) || i == (878) || i == (880) || i == (881) || i == (882) || i == (884) || i == (885) || i == (886) || i == (888) || i == (889) || i == (890) || i == (892) || i == (893) || i == (894) || i == (896) || i == (897) || i == (898) || i == (899) || i == (900) || i == (902) || i == (903) || i == (905) || i == (906) || i == (907) || i == (909) || i == (910) || i == (911) || i == (913) || i == (914) || i == (915) || i == (917) || i == (918) || i == (919) || i == (921) || i == (922) || i == (923) || i == (925) || i == (926) || i == (927) || i == (929) || i == (930) || i == (931) || i == (933) || i == (934) || i == (935) || i == (937) || i == (938) || i == (939) || i == (941) || i == (942) || i == (943) || i == (945) || i == (946) || i == (947) || i == (948) || i == (950) || i == (951) || i == (952) || i == (954) || i == (955) || i == (956) || i == (958) || i == (959) || i == (960) || i == (962) || i == (963) || i == (964) || i == (966) || i == (967) || i == (968) || i == (970) || i == (971) || i == (972) || i == (974) || i == (975) || i == (976) || i == (978) || i == (979) || i == (980) || i == (982) || i == (983) || i == (984) || i == (986) || i == (987) || i == (988) || i == (990) || i == (991) || i == (992) || i == (993) || i == (994) || i == (996) || i == (997) || i == (999) || i == (1000) || i == (1001) || i == (1003) || i == (1004) || i == (1005) || i == (1007) || i == (1008) || i == (1009) || i == (1011) || i == (1012) || i == (1013) || i == (1015) || i == (1016) || i == (1017) || i == (1019) || i == (1020) || i == (1021) || i == (1023) || i == (1024) || i == (1025) (../plain/gauss_sum.i:32:5)
[Warning][Witness] couldn't locate invariant: i == (1) || i == (2) || i == (4) || i == (5) || i == (8) || i == (9) || i == (12) || i == (13) || i == (16) || i == (17) || i == (20) || i == (21) || i == (24) || i == (25) || i == (28) || i == (29) || i == (32) || i == (33) || i == (36) || i == (37) || i == (40) || i == (41) || i == (44) || i == (45) || i == (48) || i == (49) || i == (52) || i == (53) || i == (56) || i == (57) || i == (60) || i == (61) || i == (64) || i == (65) || i == (68) || i == (69) || i == (72) || i == (73) || i == (76) || i == (77) || i == (80) || i == (81) || i == (84) || i == (85) || i == (88) || i == (89) || i == (92) || i == (93) || i == (96) || i == (97) || i == (100) || i == (101) || i == (104) || i == (105) || i == (108) || i == (109) || i == (112) || i == (113) || i == (116) || i == (117) || i == (120) || i == (121) || i == (124) || i == (125) || i == (128) || i == (129) || i == (132) || i == (133) || i == (136) || i == (137) || i == (140) || i == (141) || i == (144) || i == (145) || i == (148) || i == (149) || i == (152) || i == (153) || i == (156) || i == (157) || i == (160) || i == (161) || i == (164) || i == (165) || i == (168) || i == (169) || i == (172) || i == (173) || i == (176) || i == (177) || i == (180) || i == (181) || i == (184) || i == (185) || i == (188) || i == (189) || i == (192) || i == (193) || i == (196) || i == (197) || i == (200) || i == (201) || i == (204) || i == (205) || i == (208) || i == (209) || i == (212) || i == (213) || i == (216) || i == (217) || i == (220) || i == (221) || i == (224) || i == (225) || i == (228) || i == (229) || i == (232) || i == (233) || i == (236) || i == (237) || i == (240) || i == (241) || i == (244) || i == (245) || i == (248) || i == (249) || i == (252) || i == (253) || i == (256) || i == (257) || i == (260) || i == (261) || i == (264) || i == (265) || i == (268) || i == (269) || i == (272) || i == (273) || i == (276) || i == (277) || i == (280) || i == (281) || i == (284) || i == (285) || i == (288) || i == (289) || i == (292) || i == (293) || i == (296) || i == (297) || i == (300) || i == (301) || i == (304) || i == (305) || i == (308) || i == (309) || i == (312) || i == (313) || i == (316) || i == (317) || i == (320) || i == (321) || i == (324) || i == (325) || i == (328) || i == (329) || i == (332) || i == (333) || i == (336) || i == (337) || i == (339) || i == (340) || i == (342) || i == (343) || i == (345) || i == (346) || i == (347) || i == (349) || i == (350) || i == (351) || i == (353) || i == (354) || i == (355) || i == (357) || i == (358) || i == (359) || i == (361) || i == (362) || i == (363) || i == (365) || i == (366) || i == (368) || i == (369) || i == (370) || i == (372) || i == (373) || i == (374) || i == (376) || i == (377) || i == (378) || i == (380) || i == (381) || i == (382) || i == (384) || i == (385) || i == (386) || i == (388) || i == (389) || i == (390) || i == (392) || i == (393) || i == (394) || i == (396) || i == (397) || i == (398) || i == (400) || i == (401) || i == (402) || i == (404) || i == (405) || i == (406) || i == (408) || i == (409) || i == (410) || i == (412) || i == (413) || i == (415) || i == (417) || i == (418) || i == (421) || i == (422) || i == (425) || i == (426) || i == (429) || i == (430) || i == (432) || i == (433) || i == (435) || i == (436) || i == (438) || i == (439) || i == (440) || i == (442) || i == (443) || i == (444) || i == (446) || i == (447) || i == (448) || i == (450) || i == (451) || i == (452) || i == (454) || i == (455) || i == (456) || i == (457) || i == (459) || i == (460) || i == (461) || i == (463) || i == (464) || i == (465) || i == (467) || i == (468) || i == (469) || i == (471) || i == (472) || i == (473) || i == (475) || i == (476) || i == (477) || i == (479) || i == (480) || i == (481) || i == (483) || i == (484) || i == (485) || i == (487) || i == (488) || i == (489) || i == (491) || i == (492) || i == (493) || i == (495) || i == (496) || i == (497) || i == (499) || i == (500) || i == (501) || i == (502) || i == (503) || i == (505) || i == (506) || i == (508) || i == (509) || i == (510) || i == (512) || i == (513) || i == (514) || i == (516) || i == (517) || i == (518) || i == (520) || i == (521) || i == (522) || i == (524) || i == (525) || i == (526) || i == (528) || i == (529) || i == (530) || i == (532) || i == (533) || i == (534) || i == (536) || i == (537) || i == (538) || i == (540) || i == (541) || i == (542) || i == (544) || i == (545) || i == (546) || i == (548) || i == (549) || i == (550) || i == (552) || i == (553) || i == (555) || i == (556) || i == (557) || i == (559) || i == (560) || i == (561) || i == (563) || i == (564) || i == (565) || i == (567) || i == (568) || i == (569) || i == (571) || i == (572) || i == (573) || i == (575) || i == (576) || i == (577) || i == (579) || i == (580) || i == (581) || i == (583) || i == (584) || i == (585) || i == (587) || i == (588) || i == (589) || i == (591) || i == (592) || i == (593) || i == (595) || i == (596) || i == (597) || i == (599) || i == (600) || i == (602) || i == (603) || i == (604) || i == (606) || i == (607) || i == (608) || i == (610) || i == (611) || i == (612) || i == (614) || i == (615) || i == (616) || i == (618) || i == (619) || i == (620) || i == (621) || i == (623) || i == (624) || i == (625) || i == (627) || i == (628) || i == (629) || i == (631) || i == (632) || i == (633) || i == (635) || i == (636) || i == (637) || i == (639) || i == (640) || i == (641) || i == (643) || i == (644) || i == (645) || i == (647) || i == (648) || i == (649) || i == (651) || i == (652) || i == (653) || i == (655) || i == (656) || i == (657) || i == (659) || i == (660) || i == (661) || i == (663) || i == (664) || i == (665) || i == (666) || i == (667) || i == (669) || i == (670) || i == (672) || i == (673) || i == (674) || i == (676) || i == (677) || i == (678) || i == (680) || i == (681) || i == (682) || i == (684) || i == (685) || i == (686) || i == (688) || i == (689) || i == (690) || i == (692) || i == (693) || i == (694) || i == (696) || i == (697) || i == (698) || i == (700) || i == (701) || i == (702) || i == (704) || i == (705) || i == (706) || i == (708) || i == (709) || i == (710) || i == (712) || i == (713) || i == (714) || i == (715) || i == (717) || i == (718) || i == (719) || i == (721) || i == (722) || i == (723) || i == (725) || i == (726) || i == (727) || i == (729) || i == (730) || i == (731) || i == (733) || i == (734) || i == (735) || i == (737) || i == (738) || i == (739) || i == (741) || i == (742) || i == (743) || i == (745) || i == (746) || i == (747) || i == (749) || i == (750) || i == (751) || i == (753) || i == (754) || i == (755) || i == (757) || i == (758) || i == (759) || i == (760) || i == (761) || i == (763) || i == (764) || i == (766) || i == (767) || i == (768) || i == (770) || i == (771) || i == (772) || i == (774) || i == (775) || i == (776) || i == (778) || i == (779) || i == (780) || i == (782) || i == (783) || i == (784) || i == (786) || i == (787) || i == (788) || i == (790) || i == (791) || i == (792) || i == (794) || i == (795) || i == (796) || i == (799) || i == (800) || i == (803) || i == (804) || i == (806) || i == (807) || i == (809) || i == (810) || i == (812) || i == (813) || i == (814) || i == (816) || i == (817) || i == (818) || i == (820) || i == (821) || i == (822) || i == (824) || i == (825) || i == (826) || i == (828) || i == (829) || i == (830) || i == (832) || i == (833) || i == (835) || i == (836) || i == (837) || i == (839) || i == (840) || i == (841) || i == (843) || i == (844) || i == (845) || i == (847) || i == (848) || i == (849) || i == (851) || i == (852) || i == (853) || i == (854) || i == (856) || i == (857) || i == (858) || i == (860) || i == (861) || i == (862) || i == (864) || i == (865) || i == (866) || i == (868) || i == (869) || i == (870) || i == (872) || i == (873) || i == (874) || i == (876) || i == (877) || i == (878) || i == (880) || i == (881) || i == (882) || i == (884) || i == (885) || i == (886) || i == (888) || i == (889) || i == (890) || i == (892) || i == (893) || i == (894) || i == (896) || i == (897) || i == (898) || i == (899) || i == (900) || i == (902) || i == (903) || i == (905) || i == (906) || i == (907) || i == (909) || i == (910) || i == (911) || i == (913) || i == (914) || i == (915) || i == (917) || i == (918) || i == (919) || i == (921) || i == (922) || i == (923) || i == (925) || i == (926) || i == (927) || i == (929) || i == (930) || i == (931) || i == (933) || i == (934) || i == (935) || i == (937) || i == (938) || i == (939) || i == (941) || i == (942) || i == (943) || i == (945) || i == (946) || i == (947) || i == (948) || i == (950) || i == (951) || i == (952) || i == (954) || i == (955) || i == (956) || i == (958) || i == (959) || i == (960) || i == (962) || i == (963) || i == (964) || i == (966) || i == (967) || i == (968) || i == (970) || i == (971) || i == (972) || i == (974) || i == (975) || i == (976) || i == (978) || i == (979) || i == (980) || i == (982) || i == (983) || i == (984) || i == (986) || i == (987) || i == (988) || i == (990) || i == (991) || i == (992) || i == (993) || i == (994) || i == (996) || i == (997) || i == (999) || i == (1000) || i == (1001) || i == (1003) || i == (1004) || i == (1005) || i == (1007) || i == (1008) || i == (1009) || i == (1011) || i == (1012) || i == (1013) || i == (1015) || i == (1016) || i == (1017) || i == (1019) || i == (1020) || i == (1021) || i == (1023) || i == (1024) || i == (1025) (../plain/gauss_sum.i:30:9)
[Info][Witness] unassume invariant: sum == 0 (../plain/gauss_sum.i:29:8-29:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/gauss_sum.i:30:9-30:22)
[Info][Witness] unassume invariant: sum == 0 (../plain/gauss_sum.i:29:8-29:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/gauss_sum.i:32:5-32:40)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/gauss_sum.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/gauss_sum.i:12:73-12:74)
[Warning][Witness] invariant unconfirmed: sum == (0) (../plain/gauss_sum.i:29:5)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 1
  refuted: 0
  error: 2
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 3
SV-COMP result: unknown

vars = 35    evals = 39    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                            0.079s     0.080s     45.80MB      1×
  preprocess                         0.025s     0.024s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.13MB      4×
  Cabs2cil                           0.006s     0.006s      4.74MB      4×
  mergeCIL                           0.003s     0.003s      3.34MB      1×
  analysis                           0.036s     0.037s     28.63MB      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.02MB      2×
    Cabs2cil                           0.001s     0.001s      0.22MB      2×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            0.025s     0.025s     17.61MB      1×
      S.Dom.equal                        0.001s     0.001s      0.02MB     40×
      base unassume                      0.001s     0.001s      0.62MB     11×
      cheap_full_reach                   0.001s     0.001s      0.02MB      1×
      postsolver                         0.008s     0.008s      6.28MB      1×
        postsolver_iter                    0.008s     0.008s      6.24MB      1×
    warn_global                        0.001s     0.001s      0.11MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
