If you're having trouble understanding the error messages generated by Boogie on DafnyCC-generated code, try the following. Hand-edit the .bpl file to add {:expand} after the word 'implementation' and before the name of the problematic method. Then, re-run boogie.exe on that file.

Last edited Oct 15, 2014 at 12:13 AM by howell, version 1

Comments

No comments yet.