/opt/local/bin/civl-1.7.1 verify -inputN=6  -input_mpi_nprocs_hi=6 odd-even-par.cvl
CIVL v1.17.1 of 2018-07-30 -- http://vsl.cis.udel.edu/civl
18s: mem=31403Mb trans=40527 traceSteps=15936 explored=40532 saved=24701 prove=315
33s: mem=31403Mb trans=84118 traceSteps=33356 explored=84124 saved=51715 prove=648
48s: mem=31403Mb trans=128501 traceSteps=51226 explored=128507 saved=79448 prove=977
63s: mem=31403Mb trans=171678 traceSteps=68500 explored=171683 saved=106182 prove=1308
78s: mem=31403Mb trans=212916 traceSteps=85225 explored=212921 saved=132177 prove=1660
93s: mem=31403Mb trans=256135 traceSteps=102367 explored=256141 saved=158782 prove=2025
108s: mem=31403Mb trans=299383 traceSteps=119721 explored=299389 saved=185765 prove=2372
123s: mem=32480Mb trans=342428 traceSteps=137108 explored=342434 saved=212743 prove=2731
138s: mem=32474Mb trans=382585 traceSteps=153223 explored=382590 saved=237734 prove=3070
153s: mem=32474Mb trans=422819 traceSteps=169474 explored=422825 saved=263052 prove=3440
168s: mem=32470Mb trans=463748 traceSteps=185844 explored=463754 saved=288522 prove=3818
183s: mem=32470Mb trans=507553 traceSteps=203555 explored=507560 saved=315872 prove=4120
198s: mem=32477Mb trans=551790 traceSteps=221592 explored=551797 saved=343944 prove=4407
213s: mem=32477Mb trans=593928 traceSteps=238681 explored=593935 saved=370628 prove=4724
228s: mem=32326Mb trans=634510 traceSteps=254824 explored=634516 saved=395640 prove=5023
243s: mem=32387Mb trans=676445 traceSteps=271894 explored=676452 saved=422125 prove=5305
258s: mem=32387Mb trans=717834 traceSteps=288804 explored=717840 saved=448444 prove=5593
273s: mem=32219Mb trans=755412 traceSteps=304093 explored=755419 saved=472428 prove=5922
288s: mem=32278Mb trans=794355 traceSteps=319535 explored=794362 saved=496514 prove=6241
303s: mem=32278Mb trans=832144 traceSteps=334743 explored=832151 saved=520108 prove=6557
318s: mem=32088Mb trans=874981 traceSteps=351825 explored=874987 saved=546744 prove=6843
333s: mem=32088Mb trans=916119 traceSteps=368414 explored=916124 saved=572631 prove=7130
348s: mem=32142Mb trans=957857 traceSteps=385493 explored=957863 saved=599291 prove=7447
363s: mem=31933Mb trans=995641 traceSteps=400702 explored=995647 saved=622831 prove=7787
378s: mem=31933Mb trans=1036030 traceSteps=417052 explored=1036037 saved=648359 prove=8066
393s: mem=31920Mb trans=1073299 traceSteps=432317 explored=1073305 saved=672145 prove=8376
408s: mem=31920Mb trans=1113713 traceSteps=448794 explored=1113719 saved=697869 prove=8697
423s: mem=31858Mb trans=1149946 traceSteps=463366 explored=1149953 saved=720600 prove=9038
438s: mem=31695Mb trans=1188646 traceSteps=478539 explored=1188653 saved=744229 prove=9351
453s: mem=31695Mb trans=1227631 traceSteps=494263 explored=1227637 saved=768518 prove=9647
468s: mem=31840Mb trans=1264809 traceSteps=509145 explored=1264815 saved=791417 prove=9937
483s: mem=31855Mb trans=1302409 traceSteps=524355 explored=1302416 saved=814993 prove=10237
498s: mem=31855Mb trans=1339178 traceSteps=538978 explored=1339185 saved=837552 prove=10529
513s: mem=31886Mb trans=1376871 traceSteps=554200 explored=1376877 saved=861318 prove=10790
528s: mem=31859Mb trans=1415153 traceSteps=569987 explored=1415160 saved=885880 prove=11062
543s: mem=31859Mb trans=1451884 traceSteps=584715 explored=1451890 saved=908890 prove=11353
558s: mem=31957Mb trans=1488911 traceSteps=599786 explored=1488918 saved=932329 prove=11644
573s: mem=31957Mb trans=1524163 traceSteps=614072 explored=1524170 saved=954415 prove=11924
588s: mem=31929Mb trans=1558764 traceSteps=628165 explored=1558770 saved=976378 prove=12183
603s: mem=31929Mb trans=1594945 traceSteps=642933 explored=1594951 saved=999455 prove=12460
618s: mem=31986Mb trans=1627278 traceSteps=656088 explored=1627285 saved=1020078 prove=12766
633s: mem=31975Mb trans=1661924 traceSteps=669865 explored=1661930 saved=1041541 prove=13051
648s: mem=31975Mb trans=1694591 traceSteps=683442 explored=1694597 saved=1062613 prove=13371
663s: mem=31991Mb trans=1730612 traceSteps=697550 explored=1730618 saved=1084680 prove=13679
678s: mem=31991Mb trans=1766686 traceSteps=712230 explored=1766692 saved=1107546 prove=13933
693s: mem=31990Mb trans=1801748 traceSteps=726303 explored=1801755 saved=1129626 prove=14210
708s: mem=31990Mb trans=1837714 traceSteps=741047 explored=1837721 saved=1152612 prove=14506
723s: mem=32009Mb trans=1873187 traceSteps=755314 explored=1873194 saved=1174916 prove=14817
738s: mem=32009Mb trans=1908216 traceSteps=769589 explored=1908223 saved=1196957 prove=15130
753s: mem=31998Mb trans=1942997 traceSteps=783708 explored=1943003 saved=1219057 prove=15398
768s: mem=31998Mb trans=1976992 traceSteps=797572 explored=1976999 saved=1240778 prove=15683
783s: mem=32067Mb trans=2009509 traceSteps=810593 explored=2009516 saved=1261193 prove=15981
798s: mem=32067Mb trans=2043012 traceSteps=824486 explored=2043018 saved=1282904 prove=16297
813s: mem=32033Mb trans=2076337 traceSteps=837895 explored=2076344 saved=1303733 prove=16604
828s: mem=32033Mb trans=2111630 traceSteps=851946 explored=2111636 saved=1325755 prove=16942
843s: mem=32108Mb trans=2148809 traceSteps=866618 explored=2148818 saved=1348593 prove=17218
858s: mem=32099Mb trans=2185588 traceSteps=881153 explored=2185594 saved=1371295 prove=17506
873s: mem=32099Mb trans=2221103 traceSteps=895307 explored=2221109 saved=1393196 prove=17804
888s: mem=32051Mb trans=2258078 traceSteps=909812 explored=2258084 saved=1415957 prove=18082
903s: mem=32051Mb trans=2291400 traceSteps=923137 explored=2291406 saved=1436723 prove=18396
918s: mem=31870Mb trans=2326402 traceSteps=936886 explored=2326409 saved=1457961 prove=18672
933s: mem=31870Mb trans=2361725 traceSteps=951085 explored=2361732 saved=1480222 prove=18898
948s: mem=32035Mb trans=2396538 traceSteps=965178 explored=2396544 saved=1502253 prove=19149
963s: mem=32035Mb trans=2431063 traceSteps=979198 explored=2431069 saved=1524289 prove=19410
978s: mem=32047Mb trans=2464542 traceSteps=992534 explored=2464549 saved=1545126 prove=19673
993s: mem=32047Mb trans=2498315 traceSteps=1006001 explored=2498321 saved=1566105 prove=19944
1008s: mem=32078Mb trans=2530514 traceSteps=1018922 explored=2530520 saved=1586020 prove=20216
1023s: mem=32078Mb trans=2564545 traceSteps=1032753 explored=2564551 saved=1607734 prove=20444
1038s: mem=32057Mb trans=2596966 traceSteps=1045699 explored=2596973 saved=1627980 prove=20685
1053s: mem=32057Mb trans=2630206 traceSteps=1059226 explored=2630212 saved=1649244 prove=20961
1068s: mem=32122Mb trans=2660581 traceSteps=1071582 explored=2660588 saved=1668684 prove=21234
1083s: mem=32122Mb trans=2691753 traceSteps=1084060 explored=2691760 saved=1688173 prove=21513
1098s: mem=32105Mb trans=2724252 traceSteps=1096954 explored=2724258 saved=1708363 prove=21787
1113s: mem=32105Mb trans=2755267 traceSteps=1109320 explored=2755273 saved=1727616 prove=22067
1128s: mem=32122Mb trans=2789625 traceSteps=1122984 explored=2789632 saved=1748872 prove=22313
1143s: mem=32122Mb trans=2822373 traceSteps=1136106 explored=2822380 saved=1769356 prove=22556
1158s: mem=32126Mb trans=2853864 traceSteps=1149038 explored=2853871 saved=1789469 prove=22813
1173s: mem=32126Mb trans=2888424 traceSteps=1163087 explored=2888430 saved=1811486 prove=23090
1188s: mem=32130Mb trans=2919113 traceSteps=1175327 explored=2919119 saved=1830454 prove=23361
1203s: mem=32130Mb trans=2950717 traceSteps=1188298 explored=2950724 saved=1850626 prove=23619
1218s: mem=32127Mb trans=2981676 traceSteps=1200755 explored=2981682 saved=1870071 prove=23864
1233s: mem=32127Mb trans=3011250 traceSteps=1212650 explored=3011255 saved=1888650 prove=24137
1248s: mem=32127Mb trans=3042866 traceSteps=1225858 explored=3042873 saved=1909213 prove=24414
1263s: mem=32175Mb trans=3072654 traceSteps=1237678 explored=3072661 saved=1927762 prove=24705
1278s: mem=32175Mb trans=3103312 traceSteps=1249869 explored=3103319 saved=1946719 prove=25005
1293s: mem=32147Mb trans=3136182 traceSteps=1263135 explored=3136190 saved=1967219 prove=25243
1308s: mem=32147Mb trans=3167695 traceSteps=1276054 explored=3167701 saved=1987138 prove=25499
1323s: mem=32183Mb trans=3199681 traceSteps=1289115 explored=3199688 saved=2007251 prove=25786
1338s: mem=32183Mb trans=3230637 traceSteps=1301661 explored=3230644 saved=2026631 prove=26035
1353s: mem=32050Mb trans=3260770 traceSteps=1314136 explored=3260776 saved=2045911 prove=26303
1368s: mem=32050Mb trans=3291049 traceSteps=1326643 explored=3291056 saved=2065112 prove=26572
1383s: mem=32094Mb trans=3320556 traceSteps=1338235 explored=3320562 saved=2083175 prove=26847
1398s: mem=32094Mb trans=3350868 traceSteps=1350413 explored=3350875 saved=2102280 prove=27056
1413s: mem=32094Mb trans=3380994 traceSteps=1362492 explored=3381001 saved=2121202 prove=27290
1428s: mem=31991Mb trans=3412836 traceSteps=1375345 explored=3412843 saved=2141431 prove=27516
1443s: mem=31991Mb trans=3442484 traceSteps=1387391 explored=3442491 saved=2160365 prove=27781
1458s: mem=32057Mb trans=3471990 traceSteps=1399025 explored=3471997 saved=2178527 prove=28005
1473s: mem=32057Mb trans=3501745 traceSteps=1411191 explored=3501752 saved=2197488 prove=28261
1488s: mem=31895Mb trans=3530171 traceSteps=1422718 explored=3530177 saved=2215417 prove=28520
1503s: mem=31895Mb trans=3558928 traceSteps=1434317 explored=3558934 saved=2233475 prove=28749
1518s: mem=32039Mb trans=3586202 traceSteps=1445263 explored=3586208 saved=2250609 prove=28960
1533s: mem=32039Mb trans=3615175 traceSteps=1456706 explored=3615181 saved=2268635 prove=29201
1548s: mem=32039Mb trans=3644199 traceSteps=1468697 explored=3644205 saved=2287511 prove=29443
1563s: mem=31846Mb trans=3671595 traceSteps=1479732 explored=3671601 saved=2304855 prove=29689
1578s: mem=31846Mb trans=3699452 traceSteps=1490943 explored=3699458 saved=2322440 prove=29943
1593s: mem=32027Mb trans=3726686 traceSteps=1501766 explored=3726692 saved=2339349 prove=30195
1608s: mem=32027Mb trans=3756404 traceSteps=1513730 explored=3756411 saved=2358125 prove=30450
1623s: mem=32027Mb trans=3784890 traceSteps=1525151 explored=3784896 saved=2376070 prove=30732
1638s: mem=31820Mb trans=3814213 traceSteps=1536768 explored=3814219 saved=2394154 prove=30994
1653s: mem=31820Mb trans=3842281 traceSteps=1548103 explored=3842288 saved=2411810 prove=31208
1668s: mem=32022Mb trans=3870605 traceSteps=1559372 explored=3870612 saved=2429453 prove=31451
1683s: mem=32022Mb trans=3898179 traceSteps=1570695 explored=3898185 saved=2447143 prove=31677
1698s: mem=31806Mb trans=3927273 traceSteps=1582522 explored=3927280 saved=2465648 prove=31928
1713s: mem=31806Mb trans=3955676 traceSteps=1594066 explored=3955682 saved=2483658 prove=32186
1728s: mem=31806Mb trans=3985529 traceSteps=1606196 explored=3985535 saved=2502477 prove=32459
1743s: mem=32049Mb trans=4012866 traceSteps=1617328 explored=4012874 saved=2519796 prove=32701
1758s: mem=32049Mb trans=4039264 traceSteps=1628086 explored=4039270 saved=2536562 prove=32936
1773s: mem=32025Mb trans=4065368 traceSteps=1638582 explored=4065374 saved=2553066 prove=33163
1788s: mem=32025Mb trans=4090472 traceSteps=1648696 explored=4090478 saved=2568950 prove=33401
1803s: mem=32025Mb trans=4118329 traceSteps=1660229 explored=4118336 saved=2586914 prove=33666
1818s: mem=32076Mb trans=4144423 traceSteps=1670693 explored=4144430 saved=2603406 prove=33933
1834s: mem=32076Mb trans=4172311 traceSteps=1682049 explored=4172318 saved=2620910 prove=34191
1849s: mem=32069Mb trans=4200591 traceSteps=1693232 explored=4200597 saved=2638470 prove=34472
1864s: mem=32069Mb trans=4230096 traceSteps=1704950 explored=4230102 saved=2656733 prove=34704
1879s: mem=32069Mb trans=4259957 traceSteps=1716781 explored=4259963 saved=2675214 prove=34945
1894s: mem=32098Mb trans=4288261 traceSteps=1728273 explored=4288268 saved=2693098 prove=35195
1909s: mem=32098Mb trans=4317966 traceSteps=1740343 explored=4317972 saved=2711799 prove=35456
1924s: mem=32087Mb trans=4347981 traceSteps=1752428 explored=4347988 saved=2730446 prove=35704
1939s: mem=32087Mb trans=4375626 traceSteps=1763575 explored=4375632 saved=2747807 prove=35954
1954s: mem=32087Mb trans=4404680 traceSteps=1775052 explored=4404687 saved=2765846 prove=36185
1969s: mem=32123Mb trans=4432215 traceSteps=1786148 explored=4432221 saved=2783212 prove=36448
1984s: mem=32123Mb trans=4460171 traceSteps=1797486 explored=4460177 saved=2800722 prove=36701
1999s: mem=32110Mb trans=4488154 traceSteps=1808748 explored=4488161 saved=2818099 prove=36980

=== Source files ===
odd-even-par.cvl  (odd-even-par.cvl)


=== Command ===
civl verify -inputN=6 -input_mpi_nprocs_hi=6 odd-even-par.cvl 

=== Stats ===
   time (s)            : 1999.69
   memory (bytes)      : 33670299648
   max process count   : 7
   states              : 4491620
   states saved        : 2820179
   state matches       : 0
   transitions         : 4491613
   trace steps         : 1810069
   valid calls         : 12152497
   provers             : z3
   prover calls        : 37006

=== Result ===
The standard properties hold for all executions.
