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 14, 2014 at 11:13 PM by howell, version 1

Comments

No comments yet.