>>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=2 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 1.02 memory (bytes) : 514850816 max process count : 3 states : 87 states saved : 80 state matches : 1 transitions : 85 trace steps : 52 valid calls : 72 provers : z3 prover calls : 2 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=3 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 0.32 memory (bytes) : 514850816 max process count : 4 states : 205 states saved : 194 state matches : 6 transitions : 207 trace steps : 136 valid calls : 165 provers : z3 prover calls : 5 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=4 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 0.38 memory (bytes) : 514850816 max process count : 5 states : 476 states saved : 450 state matches : 23 transitions : 494 trace steps : 337 valid calls : 373 provers : z3 prover calls : 8 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=5 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 0.42 memory (bytes) : 514850816 max process count : 6 states : 1100 states saved : 1028 state matches : 72 transitions : 1166 trace steps : 811 valid calls : 852 provers : z3 prover calls : 11 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=6 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 0.52 memory (bytes) : 514850816 max process count : 7 states : 2525 states saved : 2328 state matches : 201 transitions : 2719 trace steps : 1910 valid calls : 1954 provers : z3 prover calls : 14 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=7 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 0.63 memory (bytes) : 514850816 max process count : 8 states : 5743 states saved : 5230 state matches : 522 transitions : 6257 trace steps : 4418 valid calls : 4463 provers : z3 prover calls : 17 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=8 ../..//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 : 10107 provers : z3 prover calls : 20 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=9 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 1.2 memory (bytes) : 640679936 max process count : 10 states : 28822 states saved : 25760 state matches : 3084 transitions : 31896 trace steps : 22621 valid calls : 22662 provers : z3 prover calls : 23 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=10 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 1.83 memory (bytes) : 906493952 max process count : 11 states : 63659 states saved : 56508 state matches : 7181 transitions : 70829 trace steps : 50284 valid calls : 50320 provers : z3 prover calls : 26 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=11 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 2.68 memory (bytes) : 1230503936 max process count : 12 states : 139457 states saved : 123098 state matches : 16398 transitions : 155843 trace steps : 110716 valid calls : 110745 provers : z3 prover calls : 29 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=12 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 4.75 memory (bytes) : 2570584064 max process count : 13 states : 303320 states saved : 266490 state matches : 36879 transitions : 340186 trace steps : 241805 valid calls : 241825 provers : z3 prover calls : 32 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=13 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 10.6 memory (bytes) : 3167223808 max process count : 14 states : 655600 states saved : 573724 state matches : 81936 transitions : 737522 trace steps : 524447 valid calls : 524456 provers : z3 prover calls : 35 === Result === The standard properties hold for all executions. >>>>>>>> Adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl 16s: mem=3084Mb trans=1157560 traceSteps=823541 explored=1025058 saved=892569 prove=38 === Source files === adder.cvl (../../examples/concurrency/adder.cvl) === Command === civl verify -inputB=14 ../..//examples/concurrency/adder.cvl === Stats === time (s) : 23.1 memory (bytes) : 3778543616 max process count : 15 states : 1409289 states saved : 1229120 state matches : 180241 transitions : 1589515 trace steps : 1130674 valid calls : 1130670 provers : z3 prover calls : 38 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === barrier.cvl (../../examples/concurrency/barrier.cvl) === Command === civl verify -inputB=2 ../..//examples/concurrency/barrier.cvl === Stats === time (s) : 1.04 memory (bytes) : 514850816 max process count : 3 states : 431 states saved : 171 state matches : 40 transitions : 466 trace steps : 138 valid calls : 454 provers : z3 prover calls : 2 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === barrier.cvl (../../examples/concurrency/barrier.cvl) === Command === civl verify -inputB=3 ../..//examples/concurrency/barrier.cvl === Stats === time (s) : 0.37 memory (bytes) : 514850816 max process count : 4 states : 2067 states saved : 826 state matches : 376 transitions : 2436 trace steps : 788 valid calls : 2349 provers : z3 prover calls : 3 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === barrier.cvl (../../examples/concurrency/barrier.cvl) === Command === civl verify -inputB=4 ../..//examples/concurrency/barrier.cvl === Stats === time (s) : 0.49 memory (bytes) : 514850816 max process count : 5 states : 9801 states saved : 3950 state matches : 2460 transitions : 12252 trace steps : 4166 valid calls : 11627 provers : z3 prover calls : 4 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === barrier.cvl (../../examples/concurrency/barrier.cvl) === Command === civl verify -inputB=5 ../..//examples/concurrency/barrier.cvl === Stats === time (s) : 0.99 memory (bytes) : 649592832 max process count : 6 states : 46379 states saved : 18627 state matches : 13795 transitions : 60163 trace steps : 20895 valid calls : 56275 provers : z3 prover calls : 5 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === barrier.cvl (../../examples/concurrency/barrier.cvl) === Command === civl verify -inputB=6 ../..//examples/concurrency/barrier.cvl === Stats === time (s) : 2.42 memory (bytes) : 1447559168 max process count : 7 states : 217063 states saved : 86345 state matches : 71264 transitions : 288314 trace steps : 100914 valid calls : 267294 provers : z3 prover calls : 6 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === barrier.cvl (../../examples/concurrency/barrier.cvl) === Command === civl verify -inputB=7 ../..//examples/concurrency/barrier.cvl === Stats === time (s) : 10.0 memory (bytes) : 3128426496 max process count : 8 states : 1000367 states saved : 393748 state matches : 349994 transitions : 1350346 trace steps : 473878 valid calls : 1247627 provers : z3 prover calls : 7 === Result === The standard properties hold for all executions. >>>>>>>> Barrier <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl 16s: mem=3105Mb trans=1980598 traceSteps=708732 explored=1481230 saved=581084 prove=8 31s: mem=2997Mb trans=4015714 traceSteps=1447134 explored=2965598 saved=1190415 prove=8 46s: mem=3342Mb trans=5643197 traceSteps=1981075 explored=4148064 saved=1604592 prove=8 === Source files === barrier.cvl (../../examples/concurrency/barrier.cvl) === Command === civl verify -inputB=8 ../..//examples/concurrency/barrier.cvl === Stats === time (s) : 48.67 memory (bytes) : 3508535296 max process count : 9 states : 4540601 states saved : 1770300 state matches : 1661020 transitions : 6201604 trace steps : 2178150 valid calls : 5734495 provers : z3 prover calls : 8 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === blockAdder.cvl (../../examples/concurrency/blockAdder.cvl) === Command === civl verify -inputB=4 -inputW=2 ../..//examples/concurrency/blockAdder.cvl === Stats === time (s) : 1.24 memory (bytes) : 514850816 max process count : 3 states : 399 states saved : 190 state matches : 4 transitions : 402 trace steps : 125 valid calls : 706 provers : z3 prover calls : 11 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === blockAdder.cvl (../../examples/concurrency/blockAdder.cvl) === Command === civl verify -inputB=6 -inputW=3 ../..//examples/concurrency/blockAdder.cvl === Stats === time (s) : 0.7 memory (bytes) : 514850816 max process count : 4 states : 1196 states saved : 644 state matches : 36 transitions : 1231 trace steps : 463 valid calls : 2965 provers : z3 prover calls : 20 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === blockAdder.cvl (../../examples/concurrency/blockAdder.cvl) === Command === civl verify -inputB=8 -inputW=4 ../..//examples/concurrency/blockAdder.cvl === Stats === time (s) : 0.83 memory (bytes) : 514850816 max process count : 5 states : 3067 states saved : 1906 state matches : 184 transitions : 3250 trace steps : 1481 valid calls : 9950 provers : z3 prover calls : 29 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === blockAdder.cvl (../../examples/concurrency/blockAdder.cvl) === Command === civl verify -inputB=10 -inputW=5 ../..//examples/concurrency/blockAdder.cvl === Stats === time (s) : 1.16 memory (bytes) : 514850816 max process count : 6 states : 7436 states saved : 5322 state matches : 720 transitions : 8155 trace steps : 4391 valid calls : 29713 provers : z3 prover calls : 38 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === blockAdder.cvl (../../examples/concurrency/blockAdder.cvl) === Command === civl verify -inputB=12 -inputW=6 ../..//examples/concurrency/blockAdder.cvl === Stats === time (s) : 1.52 memory (bytes) : 514850816 max process count : 7 states : 17855 states saved : 14366 state matches : 2412 transitions : 20266 trace steps : 12373 valid calls : 82834 provers : z3 prover calls : 47 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === blockAdder.cvl (../../examples/concurrency/blockAdder.cvl) === Command === civl verify -inputB=14 -inputW=7 ../..//examples/concurrency/blockAdder.cvl === Stats === time (s) : 2.15 memory (bytes) : 644349952 max process count : 8 states : 43124 states saved : 37760 state matches : 7308 transitions : 50431 trace steps : 33503 valid calls : 220757 provers : z3 prover calls : 56 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === blockAdder.cvl (../../examples/concurrency/blockAdder.cvl) === Command === civl verify -inputB=16 -inputW=8 ../..//examples/concurrency/blockAdder.cvl === Stats === time (s) : 3.51 memory (bytes) : 1234173952 max process count : 9 states : 104715 states saved : 96898 state matches : 20656 transitions : 125370 trace steps : 87761 valid calls : 569502 provers : z3 prover calls : 65 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === blockAdder.cvl (../../examples/concurrency/blockAdder.cvl) === Command === civl verify -inputB=18 -inputW=9 ../..//examples/concurrency/blockAdder.cvl === Stats === time (s) : 7.06 memory (bytes) : 2581594112 max process count : 10 states : 254180 states saved : 243254 state matches : 55512 transitions : 309691 trace steps : 223543 valid calls : 1432321 provers : z3 prover calls : 74 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl 16s: mem=3172Mb trans=667042 traceSteps=489570 explored=540517 saved=527024 prove=83 === Source files === blockAdder.cvl (../../examples/concurrency/blockAdder.cvl) === Command === civl verify -inputB=20 -inputW=10 ../..//examples/concurrency/blockAdder.cvl === Stats === time (s) : 16.53 memory (bytes) : 3326607360 max process count : 11 states : 613471 states saved : 598702 state matches : 143620 transitions : 757090 trace steps : 556061 valid calls : 3527778 provers : z3 prover calls : 83 === Result === The standard properties hold for all executions. >>>>>>>> Block adder <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl 16s: mem=3105Mb trans=717215 traceSteps=530706 explored=575852 saved=566681 prove=92 31s: mem=3355Mb trans=1518953 traceSteps=1125613 explored=1219439 saved=1202247 prove=92 === Source files === blockAdder.cvl (../../examples/concurrency/blockAdder.cvl) === Command === civl verify -inputB=22 -inputW=11 ../..//examples/concurrency/blockAdder.cvl === Stats === time (s) : 34.68 memory (bytes) : 3434610688 max process count : 12 states : 1467356 states saved : 1447932 state matches : 360756 transitions : 1828111 trace steps : 1355663 valid calls : 8536053 provers : z3 prover calls : 92 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === dining.cvl (../../examples/concurrency/dining.cvl) === Command === civl verify -intOperationTransformer=false -inputBOUND=2 ../..//examples/concurrency/dining.cvl === Stats === time (s) : 0.98 memory (bytes) : 514850816 max process count : 3 states : 42 states saved : 30 state matches : 4 transitions : 43 trace steps : 27 valid calls : 122 provers : z3 prover calls : 0 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === dining.cvl (../../examples/concurrency/dining.cvl) === Command === civl verify -intOperationTransformer=false -inputBOUND=3 ../..//examples/concurrency/dining.cvl === Stats === time (s) : 0.27 memory (bytes) : 514850816 max process count : 4 states : 147 states saved : 103 state matches : 40 transitions : 182 trace steps : 130 valid calls : 582 provers : z3 prover calls : 2 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === dining.cvl (../../examples/concurrency/dining.cvl) === Command === civl verify -intOperationTransformer=false -inputBOUND=4 ../..//examples/concurrency/dining.cvl === Stats === time (s) : 0.31 memory (bytes) : 514850816 max process count : 5 states : 459 states saved : 306 state matches : 193 transitions : 645 trace steps : 479 valid calls : 2189 provers : z3 prover calls : 3 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === dining.cvl (../../examples/concurrency/dining.cvl) === Command === civl verify -intOperationTransformer=false -inputBOUND=5 ../..//examples/concurrency/dining.cvl === Stats === time (s) : 0.36 memory (bytes) : 514850816 max process count : 6 states : 1588 states saved : 1013 state matches : 912 transitions : 2491 trace steps : 1897 valid calls : 8743 provers : z3 prover calls : 4 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === dining.cvl (../../examples/concurrency/dining.cvl) === Command === civl verify -intOperationTransformer=false -inputBOUND=6 ../..//examples/concurrency/dining.cvl === Stats === time (s) : 0.51 memory (bytes) : 514850816 max process count : 7 states : 5086 states saved : 3135 state matches : 3341 transitions : 8416 trace steps : 6439 valid calls : 30730 provers : z3 prover calls : 5 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === dining.cvl (../../examples/concurrency/dining.cvl) === Command === civl verify -intOperationTransformer=false -inputBOUND=7 ../..//examples/concurrency/dining.cvl === Stats === time (s) : 0.97 memory (bytes) : 649592832 max process count : 8 states : 17899 states saved : 10766 state matches : 13210 transitions : 31096 trace steps : 23929 valid calls : 116652 provers : z3 prover calls : 6 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === dining.cvl (../../examples/concurrency/dining.cvl) === Command === civl verify -intOperationTransformer=false -inputBOUND=8 ../..//examples/concurrency/dining.cvl === Stats === time (s) : 2.22 memory (bytes) : 1445986304 max process count : 9 states : 56897 states saved : 33556 state matches : 44322 transitions : 101204 trace steps : 77820 valid calls : 394567 provers : z3 prover calls : 7 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === dining.cvl (../../examples/concurrency/dining.cvl) === Command === civl verify -intOperationTransformer=false -inputBOUND=9 ../..//examples/concurrency/dining.cvl === Stats === time (s) : 7.21 memory (bytes) : 3125805056 max process count : 10 states : 198388 states saved : 115248 state matches : 164564 transitions : 362935 trace steps : 279742 valid calls : 1454138 provers : z3 prover calls : 8 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl 16s: mem=3043Mb trans=770468 traceSteps=584772 explored=462383 saved=276751 prove=9 === Source files === dining.cvl (../../examples/concurrency/dining.cvl) === Command === civl verify -intOperationTransformer=false -inputBOUND=10 ../..//examples/concurrency/dining.cvl === Stats === time (s) : 20.3 memory (bytes) : 2910322688 max process count : 11 states : 619996 states saved : 355589 state matches : 528608 transitions : 1148585 trace steps : 884114 valid calls : 4776319 provers : z3 prover calls : 9 === Result === The standard properties hold for all executions. >>>>>>>> Dining philosopher <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl 16s: mem=3034Mb trans=730922 traceSteps=554462 explored=443887 saved=267491 prove=10 31s: mem=3025Mb trans=1413485 traceSteps=1092316 explored=826520 saved=505427 prove=10 46s: mem=3338Mb trans=1992662 traceSteps=1520882 explored=1215388 saved=743685 prove=10 61s: mem=3324Mb trans=2864907 traceSteps=2178687 explored=1660317 saved=974173 prove=10 76s: mem=3259Mb trans=3791764 traceSteps=2903291 explored=2064834 saved=1176437 prove=10 === Source files === dining.cvl (../../examples/concurrency/dining.cvl) === Command === civl verify -intOperationTransformer=false -inputBOUND=11 ../..//examples/concurrency/dining.cvl === Stats === time (s) : 78.06 memory (bytes) : 3407347712 max process count : 12 states : 2130737 states saved : 1209388 state matches : 1890539 transitions : 4021255 trace steps : 3099830 valid calls : 17169687 provers : z3 prover calls : 10 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === diffusion2d.c (../../examples/mpi/diffusion2d.c) === Command === civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=1 -inputNPROCSXB=1 -inputNPROCSYB=1 -enablePrintf=false ../..//examples/mpi/diffusion2d.c === Stats === time (s) : 4.09 memory (bytes) : 919076864 max process count : 2 states : 1140 states saved : 775 state matches : 0 transitions : 1138 trace steps : 538 valid calls : 2868 provers : z3 prover calls : 4 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === diffusion2d.c (../../examples/mpi/diffusion2d.c) === Command === civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=2 -inputNPROCSXB=1 -inputNPROCSYB=2 -enablePrintf=false ../..//examples/mpi/diffusion2d.c === Stats === time (s) : 2.49 memory (bytes) : 919076864 max process count : 2 states : 2284 states saved : 1629 state matches : 0 transitions : 2282 trace steps : 1141 valid calls : 6457 provers : z3 prover calls : 8 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === diffusion2d.c (../../examples/mpi/diffusion2d.c) === Command === civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=3 -inputNPROCSXB=1 -inputNPROCSYB=3 -enablePrintf=false ../..//examples/mpi/diffusion2d.c === Stats === time (s) : 2.54 memory (bytes) : 1514668032 max process count : 2 states : 3605 states saved : 2619 state matches : 0 transitions : 3603 trace steps : 1849 valid calls : 10909 provers : z3 prover calls : 11 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === diffusion2d.c (../../examples/mpi/diffusion2d.c) === Command === civl verify -inputNSTEPSB=2 -inputNXB=2 -inputNYB=2 -inputNPROCSXB=2 -inputNPROCSYB=2 -enablePrintf=false ../..//examples/mpi/diffusion2d.c === Stats === time (s) : 4.74 memory (bytes) : 2536505344 max process count : 3 states : 14327 states saved : 9800 state matches : 0 transitions : 14324 trace steps : 6713 valid calls : 46448 provers : z3 prover calls : 18 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === diffusion2d.c (../../examples/mpi/diffusion2d.c) === Command === civl verify -inputNSTEPSB=2 -inputNXB=2 -inputNYB=3 -inputNPROCSXB=2 -inputNPROCSYB=3 -enablePrintf=false ../..//examples/mpi/diffusion2d.c === Stats === time (s) : 5.69 memory (bytes) : 2545942528 max process count : 3 states : 23516 states saved : 16107 state matches : 0 transitions : 23513 trace steps : 11085 valid calls : 78933 provers : z3 prover calls : 21 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl === Source files === diffusion2d.c (../../examples/mpi/diffusion2d.c) === Command === civl verify -inputNSTEPSB=2 -inputNXB=3 -inputNYB=3 -inputNPROCSXB=3 -inputNPROCSYB=3 -enablePrintf=false ../..//examples/mpi/diffusion2d.c === Stats === time (s) : 14.92 memory (bytes) : 2967470080 max process count : 4 states : 76154 states saved : 50193 state matches : 0 transitions : 76150 trace steps : 34139 valid calls : 281960 provers : z3 prover calls : 35 === Result === The standard properties hold for all executions. >>>>>>>> Diffusion2d <<<<<<<< CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl 17s: mem=3034Mb trans=86601 traceSteps=39473 explored=86605 saved=57453 prove=38 === Source files === diffusion2d.c (../../examples/mpi/diffusion2d.c) === Command === civl verify -inputNSTEPSB=2 -inputNXB=3 -inputNYB=4 -inputNPROCSXB=3 -inputNPROCSYB=4 -enablePrintf=false ../..//examples/mpi/diffusion2d.c === Stats === time (s) : 21.01 memory (bytes) : 3183476736 max process count : 4 states : 111347 states saved : 73235 state matches : 0 transitions : 111343 trace steps : 49956 valid calls : 419906 provers : z3 prover calls : 38 === Result === The standard properties hold for all executions.