Typo in Definition of Method Merge
Unfortunately, there has been a typo in the definition of the method Merge in Problem 3 of Problem Set K. The first while loop in the definition of Merge has to loop until a.Length (not until l) to copy the whole array into mergea. We corrected the .pdf and the .txt files of the problem set. Thanks for pointing that out to us, we hope you enjoy working with Dafny now.
Your Verification Team