/opt/local/bin/civl-1.7.1 verify -inputN=6 odd-even-seq.cvl
CIVL v1.17.1 of 2018-07-30 -- http://vsl.cis.udel.edu/civl
16s: mem=31403Mb trans=19098 traceSteps=14948 explored=19098 saved=20091 prove=552
31s: mem=31403Mb trans=40375 traceSteps=31534 explored=40375 saved=42317 prove=1098
46s: mem=31403Mb trans=56462 traceSteps=44101 explored=56462 saved=58826 prove=1708
61s: mem=31403Mb trans=72576 traceSteps=56665 explored=72576 saved=75512 prove=2261
76s: mem=31403Mb trans=88475 traceSteps=68986 explored=88475 saved=91698 prove=2863
91s: mem=31403Mb trans=105052 traceSteps=81842 explored=105052 saved=108465 prove=3474
106s: mem=31403Mb trans=121283 traceSteps=94460 explored=121283 saved=124784 prove=4086
121s: mem=31403Mb trans=139968 traceSteps=109072 explored=139968 saved=144225 prove=4642
136s: mem=31403Mb trans=158031 traceSteps=123117 explored=158031 saved=162622 prove=5235
151s: mem=31403Mb trans=173456 traceSteps=135125 explored=173457 saved=178411 prove=5806
166s: mem=31403Mb trans=187804 traceSteps=146235 explored=187804 saved=192650 prove=6409
181s: mem=31403Mb trans=203922 traceSteps=158855 explored=203921 saved=209463 prove=6899
196s: mem=31403Mb trans=220488 traceSteps=171765 explored=220488 saved=226728 prove=7394
211s: mem=31403Mb trans=235809 traceSteps=183658 explored=235809 saved=242591 prove=7913
226s: mem=31403Mb trans=249724 traceSteps=194502 explored=249724 saved=256823 prove=8463
241s: mem=31403Mb trans=264678 traceSteps=206166 explored=264679 saved=272360 prove=8944
256s: mem=31403Mb trans=279348 traceSteps=217523 explored=279348 saved=287404 prove=9436
271s: mem=31403Mb trans=292329 traceSteps=227530 explored=292330 saved=300514 prove=9949
286s: mem=31403Mb trans=306231 traceSteps=238208 explored=306231 saved=314386 prove=10491
301s: mem=31403Mb trans=319630 traceSteps=248565 explored=319630 saved=327895 prove=11010
316s: mem=31403Mb trans=334335 traceSteps=259784 explored=334335 saved=342205 prove=11548
331s: mem=31403Mb trans=348442 traceSteps=270786 explored=348442 saved=356789 prove=12011
346s: mem=31403Mb trans=361848 traceSteps=281269 explored=361849 saved=370676 prove=12502
361s: mem=31403Mb trans=376632 traceSteps=292703 explored=376632 saved=385678 prove=12984
376s: mem=31403Mb trans=389632 traceSteps=302805 explored=389633 saved=398976 prove=13462
391s: mem=31403Mb trans=403128 traceSteps=313194 explored=403128 saved=412490 prove=13965
406s: mem=31403Mb trans=416797 traceSteps=323677 explored=416798 saved=425932 prove=14490
421s: mem=31403Mb trans=430216 traceSteps=334105 explored=430216 saved=439608 prove=14932
436s: mem=31403Mb trans=443643 traceSteps=344566 explored=443643 saved=453576 prove=15367
451s: mem=31403Mb trans=458537 traceSteps=356209 explored=458537 saved=469222 prove=15784
466s: mem=31762Mb trans=472032 traceSteps=366684 explored=472033 saved=483055 prove=16251
481s: mem=31762Mb trans=484855 traceSteps=376690 explored=484856 saved=496183 prove=16732
496s: mem=31762Mb trans=495957 traceSteps=385356 explored=495958 saved=507783 prove=17121
511s: mem=31762Mb trans=507226 traceSteps=394104 explored=507226 saved=519324 prove=17566
526s: mem=31762Mb trans=518859 traceSteps=403060 explored=518859 saved=531013 prove=18021
541s: mem=31762Mb trans=531287 traceSteps=412674 explored=531287 saved=543548 prove=18482
556s: mem=31762Mb trans=544801 traceSteps=423164 explored=544801 saved=557291 prove=18911
571s: mem=31690Mb trans=556673 traceSteps=432357 explored=556673 saved=569138 prove=19366
586s: mem=31690Mb trans=568110 traceSteps=441234 explored=568110 saved=580747 prove=19787
601s: mem=31690Mb trans=580686 traceSteps=450973 explored=580686 saved=593596 prove=20199
616s: mem=31690Mb trans=593376 traceSteps=460798 explored=593376 saved=606558 prove=20615
631s: mem=31690Mb trans=605558 traceSteps=470278 explored=605558 saved=618964 prove=21043
646s: mem=31690Mb trans=617064 traceSteps=479176 explored=617064 saved=630640 prove=21453
661s: mem=31690Mb trans=627609 traceSteps=487327 explored=627609 saved=641321 prove=21872
676s: mem=31690Mb trans=639122 traceSteps=496118 explored=639123 saved=652538 prove=22341
691s: mem=31872Mb trans=653131 traceSteps=506892 explored=653131 saved=666230 prove=22818
706s: mem=31872Mb trans=662998 traceSteps=514616 explored=662999 saved=676591 prove=23130
721s: mem=31872Mb trans=673768 traceSteps=522999 explored=673769 saved=687820 prove=23489
736s: mem=31872Mb trans=685140 traceSteps=531866 explored=685141 saved=699689 prove=23851
751s: mem=31872Mb trans=696009 traceSteps=540313 explored=696009 saved=711007 prove=24224
766s: mem=31872Mb trans=706164 traceSteps=548185 explored=706164 saved=721383 prove=24609
781s: mem=31872Mb trans=716119 traceSteps=555937 explored=716120 saved=731553 prove=25006
796s: mem=31872Mb trans=726247 traceSteps=563826 explored=726248 saved=742019 prove=25366
811s: mem=31861Mb trans=735926 traceSteps=571344 explored=735926 saved=752052 prove=25725
826s: mem=31861Mb trans=746407 traceSteps=579446 explored=746407 saved=762778 prove=26084
841s: mem=31861Mb trans=756185 traceSteps=587000 explored=756186 saved=772750 prove=26474
856s: mem=31861Mb trans=765563 traceSteps=594208 explored=765564 saved=782157 prove=26860
871s: mem=31861Mb trans=776216 traceSteps=602351 explored=776216 saved=792649 prove=27266
886s: mem=31861Mb trans=787109 traceSteps=610780 explored=787109 saved=803799 prove=27653
901s: mem=31861Mb trans=798085 traceSteps=619252 explored=798085 saved=814855 prove=28049
916s: mem=31861Mb trans=809710 traceSteps=628135 explored=809711 saved=826240 prove=28467
931s: mem=31861Mb trans=821308 traceSteps=636951 explored=821309 saved=837498 prove=28902
946s: mem=31929Mb trans=831340 traceSteps=644722 explored=831341 saved=847764 prove=29240
961s: mem=31929Mb trans=841811 traceSteps=652784 explored=841811 saved=858343 prove=29617
976s: mem=31929Mb trans=851957 traceSteps=660658 explored=851957 saved=868840 prove=29961
991s: mem=31929Mb trans=862124 traceSteps=668515 explored=862124 saved=879060 prove=30344
1006s: mem=31929Mb trans=872598 traceSteps=676629 explored=872598 saved=889726 prove=30729
1021s: mem=31929Mb trans=883090 traceSteps=684756 explored=883090 saved=900423 prove=31121
1036s: mem=31929Mb trans=893153 traceSteps=692474 explored=893153 saved=910517 prove=31496
1051s: mem=31929Mb trans=902337 traceSteps=699565 explored=902337 saved=919845 prove=31864
1066s: mem=31929Mb trans=913510 traceSteps=708021 explored=913510 saved=930621 prove=32243
1081s: mem=31929Mb trans=923810 traceSteps=715850 explored=923811 saved=940617 prove=32629
1096s: mem=31916Mb trans=934898 traceSteps=724253 explored=934898 saved=951225 prove=33004
1111s: mem=31916Mb trans=947365 traceSteps=733637 explored=947365 saved=963554 prove=33420
1126s: mem=31916Mb trans=960673 traceSteps=743653 explored=960674 saved=976886 prove=33865
1141s: mem=31916Mb trans=972065 traceSteps=752150 explored=972065 saved=988155 prove=34328
1156s: mem=31916Mb trans=984707 traceSteps=761612 explored=984707 saved=1000734 prove=34784
1171s: mem=31916Mb trans=997050 traceSteps=770830 explored=997051 saved=1012942 prove=35246
1186s: mem=31916Mb trans=1009338 traceSteps=780021 explored=1009338 saved=1025172 prove=35693
1201s: mem=31916Mb trans=1020717 traceSteps=788445 explored=1020717 saved=1036261 prove=36163
1216s: mem=31916Mb trans=1032915 traceSteps=797348 explored=1032915 saved=1047947 prove=36633

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


=== Command ===
civl verify -inputN=6 odd-even-seq.cvl 

=== Stats ===
   time (s)            : 1230.54
   memory (bytes)      : 33466351616
   max process count   : 1
   states              : 1041917
   states saved        : 1056397
   state matches       : 0
   transitions         : 1041916
   trace steps         : 803631
   valid calls         : 5485343
   provers             : z3
   prover calls        : 37001

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