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