[ 0:00] | load /var/obj/divine-nightly/semidbg/test/_expand/svcomp/array/copysome2_false.pkg.c/v.1000.c v.1000.c [ 0:00] | expect --result error --location v.1000.c:50 [ 0:00] | expect --trace FAULT: --trace-count 1 [ 0:00] | cc -o testcase.bc -DSIZE=1000 v.1000.c [ 0:00] | verify --max-memory 4GiB --max-time 600 --threads 2 --report-filename verify.out --solver stp --symbolic --sequential -o nofail:malloc testcase.bc [ 0:00] compiling v.1000.c [ 0:00] loading bitcode … DiOS … LART … RR … constants … done [ 0:05] booting … done [ 0:05] states per second: 46.0931 [ 0:43] state count: 1752 [ 0:43] mips: 0.29 [ 0:43] symbolic: 1 [ 2:55] [ 2:55] error found: yes [ 2:55] error trace: | [ 2:55] ASSUME (= var_1 var_1) [ 2:55] ASSUME (= var_4 var_4) [ 2:55] ASSUME (= var_7 var_7) [ 2:55] ASSUME (= var_10 var_10) [ 2:55] ASSUME (= var_13 var_13) [ 2:55] ASSUME (= var_16 var_16) [ 2:55] ASSUME (= var_19 var_19) [ 2:55] ASSUME (= var_22 var_22) [ 2:55] ASSUME (= var_25 var_25) [ 2:55] ASSUME (= var_28 var_28) [ 2:55] ASSUME (= var_31 var_31) [ 2:55] ASSUME (= var_34 var_34) [ 2:55] ASSUME (= var_37 var_37) [ 2:55] ASSUME (= var_40 var_40) [ 2:55] ASSUME (= var_43 var_43) [ 2:55] ASSUME (= var_46 var_46) [ 2:55] ASSUME (= var_49 var_49) [ 2:55] ASSUME (= var_52 var_52) [ 2:55] ASSUME (= var_55 var_55) [ 2:55] ASSUME (= var_58 var_58) [ 2:55] ASSUME (= var_61 var_61) [ 2:55] ASSUME (= var_64 var_64) [ 2:55] ASSUME (= var_67 var_67) [ 2:55] ASSUME (= var_70 var_70) [ 2:55] ASSUME (= var_73 var_73) [ 2:55] ASSUME (= var_76 var_76) [ 2:55] ASSUME (= var_79 var_79) [ 2:55] ASSUME (= var_82 var_82) [ 2:55] ASSUME (= var_85 var_85) [ 2:55] ASSUME (= var_88 var_88) [ 2:55] ASSUME (= var_91 var_91) [ 2:55] ASSUME (= var_94 var_94) [ 2:55] ASSUME (= var_97 var_97) [ 2:55] ASSUME (= var_100 var_100) [ 2:55] ASSUME (= var_103 var_103) [ 2:55] ASSUME (= var_106 var_106) [ 2:55] ASSUME (= var_109 var_109) [ 2:55] ASSUME (= var_112 var_112) [ 2:55] ASSUME (= var_115 var_115) [ 2:55] ASSUME (= var_118 var_118) [ 2:55] ASSUME (= var_121 var_121) [ 2:55] ASSUME (= var_124 var_124) [ 2:55] ASSUME (= var_127 var_127) [ 2:55] ASSUME (= var_130 var_130) [ 2:55] ASSUME (= var_133 var_133) [ 2:55] ASSUME (= var_136 var_136) [ 2:55] ASSUME (= var_139 var_139) [ 2:55] ASSUME (= var_142 var_142) [ 2:55] ASSUME (= var_145 var_145) [ 2:55] ASSUME (= var_148 var_148) [ 2:55] ASSUME (= var_151 var_151) [ 2:55] ASSUME (= var_154 var_154) [ 2:55] ASSUME (= var_157 var_157) [ 2:55] ASSUME (= var_160 var_160) [ 2:55] ASSUME (= var_163 var_163) [ 2:55] ASSUME (= var_166 var_166) [ 2:55] ASSUME (= var_169 var_169) [ 2:55] ASSUME (= var_172 var_172) [ 2:55] ASSUME (= var_175 var_175) [ 2:55] ASSUME (= var_178 var_178) [ 2:55] ASSUME (= var_181 var_181) [ 2:55] ASSUME (= var_184 var_184) [ 2:55] ASSUME (= var_187 var_187) [ 2:55] ASSUME (= var_190 var_190) [ 2:55] ASSUME (= var_193 var_193) [ 2:55] ASSUME (= var_196 var_196) [ 2:55] ASSUME (= var_199 var_199) [ 2:55] ASSUME (= var_202 var_202) [ 2:55] ASSUME (= var_205 var_205) [ 2:55] ASSUME (= var_208 var_208) [ 2:55] ASSUME (= var_211 var_211) [ 2:55] ASSUME (= var_214 var_214) [ 2:55] ASSUME (= var_217 var_217) [ 2:55] ASSUME (= var_220 var_220) [ 2:55] ASSUME (= var_223 var_223) [ 2:55] ASSUME (= var_226 var_226) [ 2:55] ASSUME (= var_229 var_229) [ 2:55] ASSUME (= var_232 var_232) [ 2:55] ASSUME (= var_235 var_235) [ 2:55] ASSUME (= var_238 var_238) [ 2:55] ASSUME (= var_241 var_241) [ 2:55] ASSUME (= var_244 var_244) [ 2:55] ASSUME (= var_247 var_247) [ 2:55] ASSUME (= var_250 var_250) [ 2:55] ASSUME (= var_253 var_253) [ 2:55] ASSUME (= var_256 var_256) [ 2:55] ASSUME (= var_259 var_259) [ 2:55] ASSUME (= var_262 var_262) [ 2:55] ASSUME (= var_265 var_265) [ 2:55] ASSUME (= var_268 var_268) [ 2:55] ASSUME (= var_271 var_271) [ 2:55] ASSUME (= var_274 var_274) [ 2:55] ASSUME (= var_277 var_277) [ 2:55] ASSUME (= var_280 var_280) [ 2:55] ASSUME (= var_283 var_283) [ 2:55] ASSUME (= var_286 var_286) [ 2:55] ASSUME (= var_289 var_289) [ 2:55] ASSUME (= var_292 var_292) [ 2:55] ASSUME (= var_295 var_295) [ 2:55] ASSUME (= var_298 var_298) [ 2:55] ASSUME (= var_301 var_301) [ 2:55] ASSUME (= var_304 var_304) [ 2:55] ASSUME (= var_307 var_307) [ 2:55] ASSUME (= var_310 var_310) [ 2:55] ASSUME (= var_313 var_313) [ 2:55] ASSUME (= var_316 var_316) [ 2:55] ASSUME (= var_319 var_319) [ 2:55] ASSUME (= var_322 var_322) [ 2:55] ASSUME (= var_325 var_325) [ 2:55] ASSUME (= var_328 var_328) [ 2:55] ASSUME (= var_331 var_331) [ 2:55] ASSUME (= var_334 var_334) [ 2:55] ASSUME (= var_337 var_337) [ 2:55] ASSUME (= var_340 var_340) [ 2:55] ASSUME (= var_343 var_343) [ 2:55] ASSUME (= var_346 var_346) [ 2:55] ASSUME (= var_349 var_349) [ 2:55] ASSUME (= var_352 var_352) [ 2:55] ASSUME (= var_355 var_355) [ 2:55] ASSUME (= var_358 var_358) [ 2:55] ASSUME (= var_361 var_361) [ 2:55] ASSUME (= var_364 var_364) [ 2:55] ASSUME (= var_367 var_367) [ 2:55] ASSUME (= var_370 var_370) [ 2:55] ASSUME (= var_373 var_373) [ 2:55] ASSUME (= var_376 var_376) [ 2:55] ASSUME (= var_379 var_379) [ 2:55] ASSUME (= var_382 var_382) [ 2:55] ASSUME (= var_385 var_385) [ 2:55] ASSUME (= var_388 var_388) [ 2:55] ASSUME (= var_391 var_391) [ 2:55] ASSUME (= var_394 var_394) [ 2:55] ASSUME (= var_397 var_397) [ 2:55] ASSUME (= var_400 var_400) [ 2:55] ASSUME (= var_403 var_403) [ 2:55] ASSUME (= var_406 var_406) [ 2:55] ASSUME (= var_409 var_409) [ 2:55] ASSUME (= var_412 var_412) [ 2:55] ASSUME (= var_415 var_415) [ 2:55] ASSUME (= var_418 var_418) [ 2:55] ASSUME (= var_421 var_421) [ 2:55] ASSUME (= var_424 var_424) [ 2:55] ASSUME (= var_427 var_427) [ 2:55] ASSUME (= var_430 var_430) [ 2:55] ASSUME (= var_433 var_433) [ 2:55] ASSUME (= var_436 var_436) [ 2:55] ASSUME (= var_439 var_439) [ 2:55] ASSUME (= var_442 var_442) [ 2:55] ASSUME (= var_445 var_445) [ 2:55] ASSUME (= var_448 var_448) [ 2:55] ASSUME (= var_451 var_451) [ 2:55] ASSUME (= var_454 var_454) [ 2:55] ASSUME (= var_457 var_457) [ 2:55] ASSUME (= var_460 var_460) [ 2:55] ASSUME (= var_463 var_463) [ 2:55] ASSUME (= var_466 var_466) [ 2:55] ASSUME (= var_469 var_469) [ 2:55] ASSUME (= var_472 var_472) [ 2:55] ASSUME (= var_475 var_475) [ 2:55] ASSUME (= var_478 var_478) [ 2:55] ASSUME (= var_481 var_481) [ 2:55] ASSUME (= var_484 var_484) [ 2:55] ASSUME (= var_487 var_487) [ 2:55] ASSUME (= var_490 var_490) [ 2:55] ASSUME (= var_493 var_493) [ 2:55] ASSUME (= var_496 var_496) [ 2:55] ASSUME (= var_499 var_499) [ 2:55] ASSUME (= var_502 var_502) [ 2:55] ASSUME (= var_505 var_505) [ 2:55] ASSUME (= var_508 var_508) [ 2:55] ASSUME (= var_511 var_511) [ 2:55] ASSUME (= var_514 var_514) [ 2:55] ASSUME (= var_517 var_517) [ 2:55] ASSUME (= var_520 var_520) [ 2:55] ASSUME (= var_523 var_523) [ 2:55] ASSUME (= var_526 var_526) [ 2:55] ASSUME (= var_529 var_529) [ 2:55] ASSUME (= var_532 var_532) [ 2:55] ASSUME (= var_535 var_535) [ 2:55] ASSUME (= var_538 var_538) [ 2:55] ASSUME (= var_541 var_541) [ 2:55] ASSUME (= var_544 var_544) [ 2:55] ASSUME (= var_547 var_547) [ 2:55] ASSUME (= var_550 var_550) [ 2:55] ASSUME (= var_553 var_553) [ 2:55] ASSUME (= var_556 var_556) [ 2:55] ASSUME (= var_559 var_559) [ 2:55] ASSUME (= var_562 var_562) [ 2:55] ASSUME (= var_565 var_565) [ 2:55] ASSUME (= var_568 var_568) [ 2:55] ASSUME (= var_571 var_571) [ 2:55] ASSUME (= var_574 var_574) [ 2:55] ASSUME (= var_577 var_577) [ 2:55] ASSUME (= var_580 var_580) [ 2:55] ASSUME (= var_583 var_583) [ 2:55] ASSUME (= var_586 var_586) [ 2:55] ASSUME (= var_589 var_589) [ 2:55] ASSUME (= var_592 var_592) [ 2:55] ASSUME (= var_595 var_595) [ 2:55] ASSUME (= var_598 var_598) [ 2:55] ASSUME (= var_601 var_601) [ 2:55] ASSUME (= var_604 var_604) [ 2:55] ASSUME (= var_607 var_607) [ 2:55] ASSUME (= var_610 var_610) [ 2:55] ASSUME (= var_613 var_613) [ 2:55] ASSUME (= var_616 var_616) [ 2:55] ASSUME (= var_619 var_619) [ 2:55] ASSUME (= var_622 var_622) [ 2:55] ASSUME (= var_625 var_625) [ 2:55] ASSUME (= var_628 var_628) [ 2:55] ASSUME (= var_631 var_631) [ 2:55] ASSUME (= var_634 var_634) [ 2:55] ASSUME (= var_637 var_637) [ 2:55] ASSUME (= var_640 var_640) [ 2:55] ASSUME (= var_643 var_643) [ 2:55] ASSUME (= var_646 var_646) [ 2:55] ASSUME (= var_649 var_649) [ 2:55] ASSUME (= var_652 var_652) [ 2:55] ASSUME (= var_655 var_655) [ 2:55] ASSUME (= var_658 var_658) [ 2:55] ASSUME (= var_661 var_661) [ 2:55] ASSUME (= var_664 var_664) [ 2:55] ASSUME (= var_667 var_667) [ 2:55] ASSUME (= var_670 var_670) [ 2:55] ASSUME (= var_673 var_673) [ 2:55] ASSUME (= var_676 var_676) [ 2:55] ASSUME (= var_679 var_679) [ 2:55] ASSUME (= var_682 var_682) [ 2:55] ASSUME (= var_685 var_685) [ 2:55] ASSUME (= var_688 var_688) [ 2:55] ASSUME (= var_691 var_691) [ 2:55] ASSUME (= var_694 var_694) [ 2:55] ASSUME (= var_697 var_697) [ 2:55] ASSUME (= var_700 var_700) [ 2:55] ASSUME (= var_703 var_703) [ 2:55] ASSUME (= var_706 var_706) [ 2:55] ASSUME (= var_709 var_709) [ 2:55] ASSUME (= var_712 var_712) [ 2:55] ASSUME (= var_715 var_715) [ 2:55] ASSUME (= var_718 var_718) [ 2:55] ASSUME (= var_721 var_721) [ 2:55] ASSUME (= var_724 var_724) [ 2:55] ASSUME (= var_727 var_727) [ 2:55] ASSUME (= var_730 var_730) [ 2:55] ASSUME (= var_733 var_733) [ 2:55] ASSUME (= var_736 var_736) [ 2:55] ASSUME (= var_739 var_739) [ 2:55] ASSUME (= var_742 var_742) [ 2:55] ASSUME (= var_745 var_745) [ 2:55] ASSUME (= var_748 var_748) [ 2:55] ASSUME (= var_751 var_751) [ 2:55] ASSUME (= var_754 var_754) [ 2:55] ASSUME (= var_757 var_757) [ 2:55] ASSUME (= var_760 var_760) [ 2:55] ASSUME (= var_763 var_763) [ 2:55] ASSUME (= var_766 var_766) [ 2:55] ASSUME (= var_769 var_769) [ 2:55] ASSUME (= var_772 var_772) [ 2:55] ASSUME (= var_775 var_775) [ 2:55] ASSUME (= var_778 var_778) [ 2:55] ASSUME (= var_781 var_781) [ 2:55] ASSUME (= var_784 var_784) [ 2:55] ASSUME (= var_787 var_787) [ 2:55] ASSUME (= var_790 var_790) [ 2:55] ASSUME (= var_793 var_793) [ 2:55] ASSUME (= var_796 var_796) [ 2:55] ASSUME (= var_799 var_799) [ 2:55] ASSUME (= var_802 var_802) [ 2:55] ASSUME (= var_805 var_805) [ 2:55] ASSUME (= var_808 var_808) [ 2:55] ASSUME (= var_811 var_811) [ 2:55] ASSUME (= var_814 var_814) [ 2:55] ASSUME (= var_817 var_817) [ 2:55] ASSUME (= var_820 var_820) [ 2:55] ASSUME (= var_823 var_823) [ 2:55] ASSUME (= var_826 var_826) [ 2:55] ASSUME (= var_829 var_829) [ 2:55] ASSUME (= var_832 var_832) [ 2:55] ASSUME (= var_835 var_835) [ 2:55] ASSUME (= var_838 var_838) [ 2:55] ASSUME (= var_841 var_841) [ 2:55] ASSUME (= var_844 var_844) [ 2:55] ASSUME (= var_847 var_847) [ 2:55] ASSUME (= var_850 var_850) [ 2:55] ASSUME (= var_853 var_853) [ 2:55] ASSUME (= var_856 var_856) [ 2:55] ASSUME (= var_859 var_859) [ 2:55] ASSUME (= var_862 var_862) [ 2:55] ASSUME (= var_865 var_865) [ 2:55] ASSUME (= var_868 var_868) [ 2:55] ASSUME (= var_871 var_871) [ 2:55] ASSUME (= var_874 var_874) [ 2:55] ASSUME (= var_877 var_877) [ 2:55] ASSUME (= var_880 var_880) [ 2:55] ASSUME (= var_883 var_883) [ 2:55] ASSUME (= var_886 var_886) [ 2:55] ASSUME (= var_889 var_889) [ 2:55] ASSUME (= var_892 var_892) [ 2:55] ASSUME (= var_895 var_895) [ 2:55] ASSUME (= var_898 var_898) [ 2:55] ASSUME (= var_901 var_901) [ 2:55] ASSUME (= var_904 var_904) [ 2:55] ASSUME (= var_907 var_907) [ 2:55] ASSUME (= var_910 var_910) [ 2:55] ASSUME (= var_913 var_913) [ 2:55] ASSUME (= var_916 var_916) [ 2:55] ASSUME (= var_919 var_919) [ 2:55] ASSUME (= var_922 var_922) [ 2:55] ASSUME (= var_925 var_925) [ 2:55] ASSUME (= var_928 var_928) [ 2:55] ASSUME (= var_931 var_931) [ 2:55] ASSUME (= var_934 var_934) [ 2:55] ASSUME (= var_937 var_937) [ 2:55] ASSUME (= var_940 var_940) [ 2:55] ASSUME (= var_943 var_943) [ 2:55] ASSUME (= var_946 var_946) [ 2:55] ASSUME (= var_949 var_949) [ 2:55] ASSUME (= var_952 var_952) [ 2:55] ASSUME (= var_955 var_955) [ 2:55] ASSUME (= var_958 var_958) [ 2:55] ASSUME (= var_961 var_961) [ 2:55] ASSUME (= var_964 var_964) [ 2:55] ASSUME (= var_967 var_967) [ 2:55] ASSUME (= var_970 var_970) [ 2:55] ASSUME (= var_973 var_973) [ 2:55] ASSUME (= var_976 var_976) [ 2:55] ASSUME (= var_979 var_979) [ 2:55] ASSUME (= var_982 var_982) [ 2:55] ASSUME (= var_985 var_985) [ 2:55] ASSUME (= var_988 var_988) [ 2:55] ASSUME (= var_991 var_991) [ 2:55] ASSUME (= var_994 var_994) [ 2:55] ASSUME (= var_997 var_997) [ 2:55] ASSUME (= var_1000 var_1000) [ 2:55] ASSUME (= var_1003 var_1003) [ 2:55] ASSUME (= var_1006 var_1006) [ 2:55] ASSUME (= var_1009 var_1009) [ 2:55] ASSUME (= var_1012 var_1012) [ 2:55] ASSUME (= var_1015 var_1015) [ 2:55] ASSUME (= var_1018 var_1018) [ 2:55] ASSUME (= var_1021 var_1021) [ 2:55] ASSUME (= var_1024 var_1024) [ 2:55] ASSUME (= var_1027 var_1027) [ 2:55] ASSUME (= var_1030 var_1030) [ 2:55] ASSUME (= var_1033 var_1033) [ 2:55] ASSUME (= var_1036 var_1036) [ 2:55] ASSUME (= var_1039 var_1039) [ 2:55] ASSUME (= var_1042 var_1042) [ 2:55] ASSUME (= var_1045 var_1045) [ 2:55] ASSUME (= var_1048 var_1048) [ 2:55] ASSUME (= var_1051 var_1051) [ 2:55] ASSUME (= var_1054 var_1054) [ 2:55] ASSUME (= var_1057 var_1057) [ 2:55] ASSUME (= var_1060 var_1060) [ 2:55] ASSUME (= var_1063 var_1063) [ 2:55] ASSUME (= var_1066 var_1066) [ 2:55] ASSUME (= var_1069 var_1069) [ 2:55] ASSUME (= var_1072 var_1072) [ 2:55] ASSUME (= var_1075 var_1075) [ 2:55] ASSUME (= var_1078 var_1078) [ 2:55] ASSUME (= var_1081 var_1081) [ 2:55] ASSUME (= var_1084 var_1084) [ 2:55] ASSUME (= var_1087 var_1087) [ 2:55] ASSUME (= var_1090 var_1090) [ 2:55] ASSUME (= var_1093 var_1093) [ 2:55] ASSUME (= var_1096 var_1096) [ 2:55] ASSUME (= var_1099 var_1099) [ 2:55] ASSUME (= var_1102 var_1102) [ 2:55] ASSUME (= var_1105 var_1105) [ 2:55] ASSUME (= var_1108 var_1108) [ 2:55] ASSUME (= var_1111 var_1111) [ 2:55] ASSUME (= var_1114 var_1114) [ 2:55] ASSUME (= var_1117 var_1117) [ 2:55] ASSUME (= var_1120 var_1120) [ 2:55] ASSUME (= var_1123 var_1123) [ 2:55] ASSUME (= var_1126 var_1126) [ 2:55] ASSUME (= var_1129 var_1129) [ 2:55] ASSUME (= var_1132 var_1132) [ 2:55] ASSUME (= var_1135 var_1135) [ 2:55] ASSUME (= var_1138 var_1138) [ 2:55] ASSUME (= var_1141 var_1141) [ 2:55] ASSUME (= var_1144 var_1144) [ 2:55] ASSUME (= var_1147 var_1147) [ 2:55] ASSUME (= var_1150 var_1150) [ 2:55] ASSUME (= var_1153 var_1153) [ 2:55] ASSUME (= var_1156 var_1156) [ 2:55] ASSUME (= var_1159 var_1159) [ 2:55] ASSUME (= var_1162 var_1162) [ 2:55] ASSUME (= var_1165 var_1165) [ 2:55] ASSUME (= var_1168 var_1168) [ 2:55] ASSUME (= var_1171 var_1171) [ 2:55] ASSUME (= var_1174 var_1174) [ 2:55] ASSUME (= var_1177 var_1177) [ 2:55] ASSUME (= var_1180 var_1180) [ 2:55] ASSUME (= var_1183 var_1183) [ 2:55] ASSUME (= var_1186 var_1186) [ 2:55] ASSUME (= var_1189 var_1189) [ 2:55] ASSUME (= var_1192 var_1192) [ 2:55] ASSUME (= var_1195 var_1195) [ 2:55] ASSUME (= var_1198 var_1198) [ 2:55] ASSUME (= var_1201 var_1201) [ 2:55] ASSUME (= var_1204 var_1204) [ 2:55] ASSUME (= var_1207 var_1207) [ 2:55] ASSUME (= var_1210 var_1210) [ 2:55] ASSUME (= var_1213 var_1213) [ 2:55] ASSUME (= var_1216 var_1216) [ 2:55] ASSUME (= var_1219 var_1219) [ 2:55] ASSUME (= var_1222 var_1222) [ 2:55] ASSUME (= var_1225 var_1225) [ 2:55] ASSUME (= var_1228 var_1228) [ 2:55] ASSUME (= var_1231 var_1231) [ 2:55] ASSUME (= var_1234 var_1234) [ 2:55] ASSUME (= var_1237 var_1237) [ 2:55] ASSUME (= var_1240 var_1240) [ 2:55] ASSUME (= var_1243 var_1243) [ 2:55] ASSUME (= var_1246 var_1246) [ 2:55] ASSUME (= var_1249 var_1249) [ 2:55] ASSUME (= var_1252 var_1252) [ 2:55] ASSUME (= var_1255 var_1255) [ 2:55] ASSUME (= var_1258 var_1258) [ 2:55] ASSUME (= var_1261 var_1261) [ 2:55] ASSUME (= var_1264 var_1264) [ 2:55] ASSUME (= var_1267 var_1267) [ 2:55] ASSUME (= var_1270 var_1270) [ 2:55] ASSUME (= var_1273 var_1273) [ 2:55] ASSUME (= var_1276 var_1276) [ 2:55] ASSUME (= var_1279 var_1279) [ 2:55] ASSUME (= var_1282 var_1282) [ 2:55] ASSUME (= var_1285 var_1285) [ 2:55] ASSUME (= var_1288 var_1288) [ 2:55] ASSUME (= var_1291 var_1291) [ 2:55] ASSUME (= var_1294 var_1294) [ 2:55] ASSUME (= var_1297 var_1297) [ 2:55] ASSUME (= var_1300 var_1300) [ 2:55] ASSUME (= var_1303 var_1303) [ 2:55] ASSUME (= var_1306 var_1306) [ 2:55] ASSUME (= var_1309 var_1309) [ 2:55] ASSUME (= var_1312 var_1312) [ 2:55] ASSUME (= var_1315 var_1315) [ 2:55] ASSUME (= var_1318 var_1318) [ 2:55] ASSUME (= var_1321 var_1321) [ 2:55] ASSUME (= var_1324 var_1324) [ 2:55] ASSUME (= var_1327 var_1327) [ 2:55] ASSUME (= var_1330 var_1330) [ 2:55] ASSUME (= var_1333 var_1333) [ 2:55] ASSUME (= var_1336 var_1336) [ 2:55] ASSUME (= var_1339 var_1339) [ 2:55] ASSUME (= var_1342 var_1342) [ 2:55] ASSUME (= var_1345 var_1345) [ 2:55] ASSUME (= var_1348 var_1348) [ 2:55] ASSUME (= var_1351 var_1351) [ 2:55] ASSUME (= var_1354 var_1354) [ 2:55] ASSUME (= var_1357 var_1357) [ 2:55] ASSUME (= var_1360 var_1360) [ 2:55] ASSUME (= var_1363 var_1363) [ 2:55] ASSUME (= var_1366 var_1366) [ 2:56] ASSUME (= var_1369 var_1369) [ 2:56] ASSUME (= var_1372 var_1372) [ 2:56] ASSUME (= var_1375 var_1375) [ 2:56] ASSUME (= var_1378 var_1378) [ 2:56] ASSUME (= var_1381 var_1381) [ 2:56] ASSUME (= var_1384 var_1384) [ 2:56] ASSUME (= var_1387 var_1387) [ 2:56] ASSUME (= var_1390 var_1390) [ 2:56] ASSUME (= var_1393 var_1393) [ 2:56] ASSUME (= var_1396 var_1396) [ 2:56] ASSUME (= var_1399 var_1399) [ 2:56] ASSUME (= var_1402 var_1402) [ 2:56] ASSUME (= var_1405 var_1405) [ 2:56] ASSUME (= var_1408 var_1408) [ 2:56] ASSUME (= var_1411 var_1411) [ 2:56] ASSUME (= var_1414 var_1414) [ 2:56] ASSUME (= var_1417 var_1417) [ 2:56] ASSUME (= var_1420 var_1420) [ 2:56] ASSUME (= var_1423 var_1423) [ 2:56] ASSUME (= var_1426 var_1426) [ 2:56] ASSUME (= var_1429 var_1429) [ 2:56] ASSUME (= var_1432 var_1432) [ 2:56] ASSUME (= var_1435 var_1435) [ 2:56] ASSUME (= var_1438 var_1438) [ 2:56] ASSUME (= var_1441 var_1441) [ 2:56] ASSUME (= var_1444 var_1444) [ 2:56] ASSUME (= var_1447 var_1447) [ 2:56] ASSUME (= var_1450 var_1450) [ 2:56] ASSUME (= var_1453 var_1453) [ 2:56] ASSUME (= var_1456 var_1456) [ 2:56] ASSUME (= var_1459 var_1459) [ 2:56] ASSUME (= var_1462 var_1462) [ 2:56] ASSUME (= var_1465 var_1465) [ 2:56] ASSUME (= var_1468 var_1468) [ 2:56] ASSUME (= var_1471 var_1471) [ 2:56] ASSUME (= var_1474 var_1474) [ 2:56] ASSUME (= var_1477 var_1477) [ 2:56] ASSUME (= var_1480 var_1480) [ 2:56] ASSUME (= var_1483 var_1483) [ 2:56] ASSUME (= var_1486 var_1486) [ 2:56] ASSUME (= var_1489 var_1489) [ 2:56] ASSUME (= var_1492 var_1492) [ 2:56] ASSUME (= var_1495 var_1495) [ 2:56] ASSUME (= var_1498 var_1498) [ 2:56] ASSUME (= var_1501 var_1501) [ 2:56] ASSUME (not (= var_1505 var_1504)) [ 2:56] FAULT: verifier error called [ 2:56] [0] FATAL: dios assertion violation in userspace [ 2:56] [ 2:56] active stack: [ 2:56] - symbol: void __dios::FaultBase::handler<__dios::Context>(_VM_Fault, _VM_Frame*, void (*)()) [ 2:56] location: /dios/sys/fault.hpp:118 [ 2:56] - symbol: __dios_fault [ 2:56] location: /dios/arch/divm/fault.c:12 [ 2:56] - symbol: __VERIFIER_error [ 2:56] location: /dios/libc/svcomp/svcomp-error.cpp:5 [ 2:56] - symbol: __VERIFIER_assert [ 2:56] location: v.1000.c:18 [ 2:56] - symbol: main [ 2:56] location: v.1000.c:50 [ 2:56] - symbol: __dios_start [ 2:56] location: /dios/libc/sys/start.cpp:91 [ 2:56] + divine sim --batch --skip-init --load-report verify.out [ 2:56] [ 3:02] ^ —————. —.— . . —.— . . .————— . . [ 3:02] ——— | | | | | | |\ | | | | [ 3:02] —(o)— | | | | | | | \ | |———— '————| [ 3:02] ——————— | | | \ / | | \| | | [ 3:02] ————————— —————' —'— ' —'— ' ' '————— ' [ 3:02] [ 3:02] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started. [ 3:02] traced states: [ 4:39] ▶ state #1751 [new] -- active threads: [0:0] -- [ 4:39] T: FAULT: verifier error called [ 4:39] # executing void __dios::FaultBase::handler<{Context}>(_VM_Fault, _VM_Frame*, void (*)()) at /dios/sys/fault.hpp:118 [ 4:39] # NOTE: $frame in __dios_fault [ 4:39] > backtrace [ 4:39] void __dios::FaultBase::handler<{Context}>(_VM_Fault, _VM_Frame*, void (*)()) at /dios/sys/fault.hpp:118 [ 4:39] __dios_fault at /dios/arch/divm/fault.c:12 [ 4:39] __VERIFIER_error at /dios/libc/svcomp/svcomp-error.cpp:5 [ 4:39] __VERIFIER_assert at v.1000.c:18 [ 4:39] main at v.1000.c:50 [ 4:39] __dios_start at /dios/libc/sys/start.cpp:91 [ 4:39] # executing void __dios::FaultBase::handler<{Context}>(_VM_Fault, _VM_Frame*, void (*)()) at /dios/sys/fault.hpp:118 [ 4:39] # NOTE: $frame in __dios_fault