summaryrefslogtreecommitdiff
path: root/Test/dafny4
ModeNameSize
-rw-r--r--ACL2-extractor.dfy6954logplain
-rw-r--r--ACL2-extractor.dfy.expect62logplain
-rw-r--r--Ackermann.dfy7160logplain
-rw-r--r--Ackermann.dfy.expect123logplain
-rw-r--r--BinarySearch.dfy2116logplain
-rw-r--r--BinarySearch.dfy.expect337logplain
-rw-r--r--Bug100.dfy493logplain
-rw-r--r--Bug100.dfy.expect61logplain
-rw-r--r--Bug101.dfy297logplain
-rw-r--r--Bug101.dfy.expect207logplain
-rw-r--r--Bug103.dfy288logplain
-rw-r--r--Bug103.dfy.expect61logplain
-rw-r--r--Bug104.dfy264logplain
-rw-r--r--Bug104.dfy.expect166logplain
-rw-r--r--Bug107.dfy183logplain
-rw-r--r--Bug107.dfy.expect107logplain
-rw-r--r--Bug108.dfy209logplain
-rw-r--r--Bug108.dfy.expect130logplain
-rw-r--r--Bug110.dfy626logplain
-rw-r--r--Bug110.dfy.expect61logplain
-rw-r--r--Bug111.dfy237logplain
-rw-r--r--Bug111.dfy.expect61logplain
-rw-r--r--Bug113.dfy186logplain
-rw-r--r--Bug113.dfy.expect126logplain
-rw-r--r--Bug114.dfy263logplain
-rw-r--r--Bug114.dfy.expect182logplain
-rw-r--r--Bug116.dfy198logplain
-rw-r--r--Bug116.dfy.expect96logplain
-rw-r--r--Bug117.dfy789logplain
-rw-r--r--Bug117.dfy.expect377logplain
-rw-r--r--Bug118.dfy288logplain
-rw-r--r--Bug118.dfy.expect61logplain
-rw-r--r--Bug120.dfy189logplain
-rw-r--r--Bug120.dfy.expect61logplain
-rw-r--r--Bug121.dfy220logplain
-rw-r--r--Bug121.dfy.expect61logplain
-rw-r--r--Bug122.dfy169logplain
-rw-r--r--Bug122.dfy.expect61logplain
-rw-r--r--Bug124.dfy344logplain
-rw-r--r--Bug124.dfy.expect61logplain
-rw-r--r--Bug125.dfy834logplain
-rw-r--r--Bug125.dfy.expect62logplain
-rw-r--r--Bug128.dfy364logplain
-rw-r--r--Bug128.dfy.expect197logplain
-rw-r--r--Bug129.dfy243logplain
-rw-r--r--Bug129.dfy.expect61logplain
-rw-r--r--Bug131.dfy159logplain
-rw-r--r--Bug131.dfy.expect113logplain
-rw-r--r--Bug133.dfy341logplain
-rw-r--r--Bug133.dfy.expect61logplain
-rw-r--r--Bug134.dfy435logplain
-rw-r--r--Bug134.dfy.expect269logplain
-rw-r--r--Bug54.dfy426logplain
-rw-r--r--Bug54.dfy.expect61logplain
-rw-r--r--Bug55.dfy253logplain
-rw-r--r--Bug55.dfy.expect61logplain
-rw-r--r--Bug56.dfy555logplain
-rw-r--r--Bug56.dfy.expect61logplain
-rw-r--r--Bug58.dfy386logplain
-rw-r--r--Bug58.dfy.expect61logplain
-rw-r--r--Bug60.dfy369logplain
-rw-r--r--Bug60.dfy.expect157logplain
-rw-r--r--Bug62.dfy547logplain
-rw-r--r--Bug62.dfy.expect61logplain
-rw-r--r--Bug63.dfy219logplain
-rw-r--r--Bug63.dfy.expect61logplain
-rw-r--r--Bug67.dfy278logplain
-rw-r--r--Bug67.dfy.expect115logplain
-rw-r--r--Bug68.dfy1432logplain
-rw-r--r--Bug68.dfy.expect142logplain
-rw-r--r--Bug69.dfy307logplain
-rw-r--r--Bug69.dfy.expect61logplain
-rw-r--r--Bug70.dfy280logplain
-rw-r--r--Bug70.dfy.expect61logplain
-rw-r--r--Bug71.dfy280logplain
-rw-r--r--Bug71.dfy.expect61logplain
-rw-r--r--Bug72.dfy464logplain
-rw-r--r--Bug73.dfy274logplain
-rw-r--r--Bug73.dfy.expect327logplain
-rw-r--r--Bug79.dfy183logplain
-rw-r--r--Bug79.dfy.expect61logplain
-rw-r--r--Bug81.dfy258logplain
-rw-r--r--Bug81.dfy.expect61logplain
-rw-r--r--Bug82.dfy242logplain
-rw-r--r--Bug82.dfy.expect61logplain
-rw-r--r--Bug88.dfy212logplain
-rw-r--r--Bug88.dfy.expect499logplain
-rw-r--r--Bug89.dfy216logplain
-rw-r--r--Bug89.dfy.expect107logplain
-rw-r--r--Bug91.dfy865logplain
-rw-r--r--Bug91.dfy.expect61logplain
-rw-r--r--Bug94.dfy436logplain
-rw-r--r--Bug94.dfy.expect108logplain
-rw-r--r--Bug99.dfy264logplain
-rw-r--r--Bug99.dfy.expect61logplain
-rw-r--r--Circ.dfy2317logplain
-rw-r--r--Circ.dfy.expect62logplain
-rw-r--r--ClassRefinement.dfy1578logplain
-rw-r--r--ClassRefinement.dfy.expect62logplain
-rw-r--r--CoqArt-InsertionSort.dfy4351logplain
-rw-r--r--CoqArt-InsertionSort.dfy.expect62logplain
-rw-r--r--FlyingRobots.dfy7527logplain
-rw-r--r--FlyingRobots.dfy.expect107logplain
-rw-r--r--Fstar-QuickSort.dfy4324logplain
-rw-r--r--Fstar-QuickSort.dfy.expect61logplain
-rw-r--r--GHC-MergeSort.dfy22257logplain
-rw-r--r--GHC-MergeSort.dfy.expect62logplain
-rw-r--r--Juggernaut.dfy335logplain
-rw-r--r--Juggernaut.dfy.expect61logplain
-rw-r--r--KozenSilva.dfy13638logplain
-rw-r--r--KozenSilva.dfy.expect62logplain
-rw-r--r--LargeConstants.dfy307logplain
-rw-r--r--LargeConstants.dfy.expect61logplain
-rw-r--r--Leq.dfy3914logplain
-rw-r--r--Leq.dfy.expect94logplain
-rw-r--r--NipkowKlein-chapter3.dfy8909logplain
-rw-r--r--NipkowKlein-chapter3.dfy.expect62logplain
-rw-r--r--NipkowKlein-chapter7.dfy11726logplain
-rw-r--r--NipkowKlein-chapter7.dfy.expect62logplain
-rw-r--r--NumberRepresentations.dfy9576logplain
-rw-r--r--NumberRepresentations.dfy.expect62logplain
-rw-r--r--Primes.dfy5974logplain
-rw-r--r--Primes.dfy.expect62logplain
-rw-r--r--Regression0.dfy371logplain
-rw-r--r--Regression0.dfy.expect352logplain
-rw-r--r--Regression1.dfy282logplain
-rw-r--r--Regression1.dfy.expect61logplain
-rw-r--r--SoftwareFoundations-Basics.dfy11485logplain
-rw-r--r--SoftwareFoundations-Basics.dfy.expect164logplain
-rw-r--r--UnionFind.dfy12507logplain
-rw-r--r--UnionFind.dfy.expect100logplain
-rw-r--r--bug72.dfy.expect61logplain
-rw-r--r--set-compr.dfy2673logplain
-rw-r--r--set-compr.dfy.expect2743logplain