This is a modified version of Dafny that can export the Dafny program as an Isabelle expression and use a modified Boogie version. The translation is also modified.
You may need to remove the BPL_EXPORT_DIR_OPTION at the beginning of
DafnyDriver.cs.
The Boogie version in Directory.Build.props
must be set to the same version used by the modified Boogie nuget package.
dafny /fragment /compile:0 /print:foo.bpl /exportDfy:foo_export foo.dfy