>>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=2 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 1.25 memory (bytes) : 514850816 max process count : 3 states : 87 states saved : 80 state matches : 1 transitions : 85 trace steps : 52 valid calls : 91 provers : cvc4, z3, cvc3 prover calls : 2 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=3 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 0.35 memory (bytes) : 514850816 max process count : 4 states : 205 states saved : 194 state matches : 6 transitions : 207 trace steps : 136 valid calls : 219 provers : cvc4, z3, cvc3 prover calls : 4 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=4 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 0.43 memory (bytes) : 514850816 max process count : 5 states : 476 states saved : 450 state matches : 23 transitions : 494 trace steps : 337 valid calls : 508 provers : cvc4, z3, cvc3 prover calls : 6 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=5 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 0.49 memory (bytes) : 514850816 max process count : 6 states : 1100 states saved : 1028 state matches : 72 transitions : 1166 trace steps : 811 valid calls : 1162 provers : cvc4, z3, cvc3 prover calls : 8 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=6 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 0.58 memory (bytes) : 514850816 max process count : 7 states : 2525 states saved : 2328 state matches : 201 transitions : 2719 trace steps : 1910 valid calls : 2629 provers : cvc4, z3, cvc3 prover calls : 10 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=7 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 0.72 memory (bytes) : 514850816 max process count : 8 states : 5743 states saved : 5230 state matches : 522 transitions : 6257 trace steps : 4418 valid calls : 5885 provers : cvc4, z3, cvc3 prover calls : 12 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=8 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 0.88 memory (bytes) : 514850816 max process count : 9 states : 12930 states saved : 11654 state matches : 1291 transitions : 14212 trace steps : 10063 valid calls : 13042 provers : cvc4, z3, cvc3 prover calls : 14 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=9 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 1.22 memory (bytes) : 504365056 max process count : 10 states : 28822 states saved : 25760 state matches : 3084 transitions : 31896 trace steps : 22621 valid calls : 28644 provers : cvc4, z3, cvc3 prover calls : 16 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=10 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 1.66 memory (bytes) : 789577728 max process count : 11 states : 63659 states saved : 56508 state matches : 7181 transitions : 70829 trace steps : 50284 valid calls : 62419 provers : cvc4, z3, cvc3 prover calls : 18 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=11 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 2.58 memory (bytes) : 1039663104 max process count : 12 states : 139457 states saved : 123098 state matches : 16398 transitions : 155843 trace steps : 110716 valid calls : 135103 provers : cvc4, z3, cvc3 prover calls : 20 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=12 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 4.68 memory (bytes) : 2087714816 max process count : 13 states : 303320 states saved : 266490 state matches : 36879 transitions : 340186 trace steps : 241805 valid calls : 290728 provers : cvc4, z3, cvc3 prover calls : 22 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=13 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 10.19 memory (bytes) : 3173515264 max process count : 14 states : 655600 states saved : 573724 state matches : 81936 transitions : 737522 trace steps : 524447 valid calls : 622478 provers : cvc4, z3, cvc3 prover calls : 24 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl 16s: mem=3098Mb trans=1175479 traceSteps=836293 explored=1040899 saved=906333 prove=26 === Command === civl verify -inputB=14 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl === Stats === time (s) : 22.57 memory (bytes) : 3839361024 max process count : 15 states : 1409289 states saved : 1229120 state matches : 180241 transitions : 1589515 trace steps : 1130674 valid calls : 1326961 provers : cvc4, z3, cvc3 prover calls : 26 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=2 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl === Stats === time (s) : 1.05 memory (bytes) : 514850816 max process count : 3 states : 431 states saved : 171 state matches : 40 transitions : 466 trace steps : 138 valid calls : 863 provers : cvc4, z3, cvc3 prover calls : 2 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=3 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl === Stats === time (s) : 0.4 memory (bytes) : 514850816 max process count : 4 states : 2067 states saved : 826 state matches : 376 transitions : 2436 trace steps : 788 valid calls : 4920 provers : cvc4, z3, cvc3 prover calls : 3 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=4 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl === Stats === time (s) : 0.51 memory (bytes) : 514850816 max process count : 5 states : 9801 states saved : 3950 state matches : 2460 transitions : 12252 trace steps : 4166 valid calls : 25118 provers : cvc4, z3, cvc3 prover calls : 4 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=5 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl === Stats === time (s) : 1.01 memory (bytes) : 649592832 max process count : 6 states : 46379 states saved : 18627 state matches : 13795 transitions : 60163 trace steps : 20895 valid calls : 122504 provers : cvc4, z3, cvc3 prover calls : 5 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=6 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl === Stats === time (s) : 2.29 memory (bytes) : 1449132032 max process count : 7 states : 217063 states saved : 86345 state matches : 71264 transitions : 288314 trace steps : 100914 valid calls : 582487 provers : cvc4, z3, cvc3 prover calls : 6 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=7 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl === Stats === time (s) : 9.29 memory (bytes) : 3127377920 max process count : 8 states : 1000367 states saved : 393748 state matches : 349994 transitions : 1350346 trace steps : 473878 valid calls : 2719222 provers : cvc4, z3, cvc3 prover calls : 7 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl 16s: mem=3104Mb trans=2009934 traceSteps=721270 explored=1503318 saved=591940 prove=8 31s: mem=2992Mb trans=4061863 traceSteps=1463553 explored=2998363 saved=1204673 prove=8 46s: mem=3311Mb trans=5831150 traceSteps=2045850 explored=4281517 saved=1657605 prove=8 === Command === civl verify -inputB=8 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl === Stats === time (s) : 47.47 memory (bytes) : 3496476672 max process count : 9 states : 4540601 states saved : 1770300 state matches : 1661020 transitions : 6201604 trace steps : 2178150 valid calls : 12507866 provers : cvc4, z3, cvc3 prover calls : 8 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=4 -inputW=2 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl === Stats === time (s) : 1.3 memory (bytes) : 514850816 max process count : 3 states : 399 states saved : 190 state matches : 4 transitions : 402 trace steps : 125 valid calls : 1167 provers : cvc4, z3, cvc3 prover calls : 8 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=6 -inputW=3 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl === Stats === time (s) : 0.79 memory (bytes) : 514850816 max process count : 4 states : 1196 states saved : 644 state matches : 36 transitions : 1231 trace steps : 463 valid calls : 4772 provers : cvc4, z3, cvc3 prover calls : 14 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=8 -inputW=4 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl === Stats === time (s) : 1.02 memory (bytes) : 514850816 max process count : 5 states : 3067 states saved : 1906 state matches : 184 transitions : 3250 trace steps : 1481 valid calls : 15639 provers : cvc4, z3, cvc3 prover calls : 20 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=10 -inputW=5 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl === Stats === time (s) : 1.3 memory (bytes) : 514850816 max process count : 6 states : 7436 states saved : 5322 state matches : 720 transitions : 8155 trace steps : 4391 valid calls : 45884 provers : cvc4, z3, cvc3 prover calls : 26 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=12 -inputW=6 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl === Stats === time (s) : 1.74 memory (bytes) : 514850816 max process count : 7 states : 17855 states saved : 14366 state matches : 2412 transitions : 20266 trace steps : 12373 valid calls : 126359 provers : cvc4, z3, cvc3 prover calls : 32 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=14 -inputW=7 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl === Stats === time (s) : 2.31 memory (bytes) : 911736832 max process count : 8 states : 43124 states saved : 37760 state matches : 7308 transitions : 50431 trace steps : 33503 valid calls : 333948 provers : cvc4, z3, cvc3 prover calls : 38 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=16 -inputW=8 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl === Stats === time (s) : 3.82 memory (bytes) : 1231552512 max process count : 9 states : 104715 states saved : 96898 state matches : 20656 transitions : 125370 trace steps : 87761 valid calls : 856463 provers : cvc4, z3, cvc3 prover calls : 44 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputB=18 -inputW=9 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl === Stats === time (s) : 7.29 memory (bytes) : 2570584064 max process count : 10 states : 254180 states saved : 243254 state matches : 55512 transitions : 309691 trace steps : 223543 valid calls : 2144708 provers : cvc4, z3, cvc3 prover calls : 50 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl 17s: mem=3179Mb trans=711270 traceSteps=522328 explored=576255 saved=562255 prove=56 === Command === civl verify -inputB=20 -inputW=10 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl === Stats === time (s) : 16.83 memory (bytes) : 3333947392 max process count : 11 states : 613471 states saved : 598702 state matches : 143620 transitions : 757090 trace steps : 556061 valid calls : 5264479 provers : cvc4, z3, cvc3 prover calls : 56 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl 16s: mem=3113Mb trans=686467 traceSteps=507735 explored=551380 saved=542323 prove=62 31s: mem=3346Mb trans=1439151 traceSteps=1066299 explored=1155411 saved=1138884 prove=62 === Command === civl verify -inputB=22 -inputW=11 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl === Stats === time (s) : 36.15 memory (bytes) : 3535798272 max process count : 12 states : 1467356 states saved : 1447932 state matches : 360756 transitions : 1828111 trace steps : 1355663 valid calls : 12702964 provers : cvc4, z3, cvc3 prover calls : 62 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -intOperationTransformer=false -inputBOUND=2 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl === Stats === time (s) : 0.96 memory (bytes) : 514850816 max process count : 3 states : 42 states saved : 30 state matches : 4 transitions : 43 trace steps : 27 valid calls : 213 provers : cvc4, z3, cvc3 prover calls : 0 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -intOperationTransformer=false -inputBOUND=3 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl === Stats === time (s) : 0.3 memory (bytes) : 514850816 max process count : 4 states : 147 states saved : 103 state matches : 40 transitions : 182 trace steps : 130 valid calls : 1149 provers : cvc4, z3, cvc3 prover calls : 2 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -intOperationTransformer=false -inputBOUND=4 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl === Stats === time (s) : 0.36 memory (bytes) : 514850816 max process count : 5 states : 459 states saved : 306 state matches : 193 transitions : 645 trace steps : 479 valid calls : 4592 provers : cvc4, z3, cvc3 prover calls : 3 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -intOperationTransformer=false -inputBOUND=5 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl === Stats === time (s) : 0.41 memory (bytes) : 514850816 max process count : 6 states : 1588 states saved : 1013 state matches : 912 transitions : 2491 trace steps : 1897 valid calls : 18932 provers : cvc4, z3, cvc3 prover calls : 4 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -intOperationTransformer=false -inputBOUND=6 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl === Stats === time (s) : 0.59 memory (bytes) : 514850816 max process count : 7 states : 5086 states saved : 3135 state matches : 3341 transitions : 8416 trace steps : 6439 valid calls : 67751 provers : cvc4, z3, cvc3 prover calls : 5 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -intOperationTransformer=false -inputBOUND=7 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl === Stats === time (s) : 1.03 memory (bytes) : 649592832 max process count : 8 states : 17899 states saved : 10766 state matches : 13210 transitions : 31096 trace steps : 23929 valid calls : 260545 provers : cvc4, z3, cvc3 prover calls : 6 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -intOperationTransformer=false -inputBOUND=8 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl === Stats === time (s) : 1.91 memory (bytes) : 1445462016 max process count : 9 states : 56897 states saved : 33556 state matches : 44322 transitions : 101204 trace steps : 77820 valid calls : 891894 provers : cvc4, z3, cvc3 prover calls : 7 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -intOperationTransformer=false -inputBOUND=9 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl === Stats === time (s) : 6.09 memory (bytes) : 3124756480 max process count : 10 states : 198388 states saved : 115248 state matches : 164564 transitions : 362935 trace steps : 279742 valid calls : 3319541 provers : cvc4, z3, cvc3 prover calls : 8 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl 16s: mem=3040Mb trans=897240 traceSteps=681675 explored=522184 saved=306683 prove=9 === Command === civl verify -intOperationTransformer=false -inputBOUND=10 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl === Stats === time (s) : 18.01 memory (bytes) : 3187146752 max process count : 11 states : 619996 states saved : 355589 state matches : 528608 transitions : 1148585 trace steps : 884114 valid calls : 11016852 provers : cvc4, z3, cvc3 prover calls : 9 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl 16s: mem=3043Mb trans=878298 traceSteps=667143 explored=513358 saved=302268 prove=10 31s: mem=3027Mb trans=1589082 traceSteps=1226082 explored=944946 saved=582022 prove=10 46s: mem=3348Mb trans=2364691 traceSteps=1795674 explored=1425838 saved=856898 prove=10 61s: mem=3309Mb trans=3435878 traceSteps=2620878 explored=1917887 saved=1102963 prove=10 === Command === civl verify -intOperationTransformer=false -inputBOUND=11 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl === Stats === time (s) : 67.52 memory (bytes) : 3448242176 max process count : 12 states : 2130737 states saved : 1209388 state matches : 1890539 transitions : 4021255 trace steps : 3099830 valid calls : 39942930 provers : cvc4, z3, cvc3 prover calls : 10 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=1 -inputNPROCSXB=1 -inputNPROCSYB=1 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c === Stats === time (s) : 4.35 memory (bytes) : 919076864 max process count : 2 states : 1140 states saved : 775 state matches : 0 transitions : 1138 trace steps : 538 valid calls : 3313 provers : cvc4, z3, cvc3 prover calls : 3 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=2 -inputNPROCSXB=1 -inputNPROCSYB=2 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c === Stats === time (s) : 2.68 memory (bytes) : 1512046592 max process count : 2 states : 2284 states saved : 1629 state matches : 0 transitions : 2282 trace steps : 1141 valid calls : 7463 provers : cvc4, z3, cvc3 prover calls : 5 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=3 -inputNPROCSXB=1 -inputNPROCSYB=3 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c === Stats === time (s) : 2.95 memory (bytes) : 1512046592 max process count : 2 states : 3605 states saved : 2619 state matches : 0 transitions : 3603 trace steps : 1849 valid calls : 12629 provers : cvc4, z3, cvc3 prover calls : 7 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputNSTEPSB=2 -inputNXB=2 -inputNYB=2 -inputNPROCSXB=2 -inputNPROCSYB=2 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c === Stats === time (s) : 4.93 memory (bytes) : 2589982720 max process count : 3 states : 14327 states saved : 9800 state matches : 0 transitions : 14324 trace steps : 6713 valid calls : 52083 provers : cvc4, z3, cvc3 prover calls : 15 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl === Command === civl verify -inputNSTEPSB=2 -inputNXB=2 -inputNYB=3 -inputNPROCSXB=2 -inputNPROCSYB=3 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c === Stats === time (s) : 6.48 memory (bytes) : 2619867136 max process count : 3 states : 23516 states saved : 16107 state matches : 0 transitions : 23513 trace steps : 11085 valid calls : 88651 provers : cvc4, z3, cvc3 prover calls : 17 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl 17s: mem=2842Mb trans=72341 traceSteps=32520 explored=72344 saved=47742 prove=34 === Command === civl verify -inputNSTEPSB=2 -inputNXB=3 -inputNYB=3 -inputNPROCSXB=3 -inputNPROCSYB=3 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c === Stats === time (s) : 17.41 memory (bytes) : 2980577280 max process count : 4 states : 76154 states saved : 50193 state matches : 0 transitions : 76150 trace steps : 34139 valid calls : 310971 provers : cvc4, z3, cvc3 prover calls : 34 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl 17s: mem=2963Mb trans=73950 traceSteps=34165 explored=73953 saved=49471 prove=36 === Command === civl verify -inputNSTEPSB=2 -inputNXB=3 -inputNYB=4 -inputNPROCSXB=3 -inputNPROCSYB=4 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c === Stats === time (s) : 24.7 memory (bytes) : 3112173568 max process count : 4 states : 111347 states saved : 73235 state matches : 0 transitions : 111343 trace steps : 49956 valid calls : 463610 provers : cvc4, z3, cvc3 prover calls : 36 === Result === The standard properties hold for all executions.