4 files changed, 1651 insertions, 0 deletions
diff --git a/Test/server/minimal.transcript b/Test/server/minimal.transcript
new file mode 100644
index 00000000..394fd921
--- /dev/null
+++ b/Test/server/minimal.transcript
@@ -0,0 +1,8 @@
+# RUN: "%server" "%s" > "%t"
+# RUN: %diff "%s.expect" "%t"
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
diff --git a/Test/server/minimal.transcript.expect b/Test/server/minimal.transcript.expect
new file mode 100644
index 00000000..bf3f9dfb
--- /dev/null
+++ b/Test/server/minimal.transcript.expect
@@ -0,0 +1,14 @@
+# Reading from minimal.transcript
+
+Verifying CheckWellformed$$_module.__default.A ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+  [2 proof obligations]  error
+transcript(3,9): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
diff --git a/Test/server/simple-session.transcript b/Test/server/simple-session.transcript
new file mode 100644
index 00000000..d095f6dd
--- /dev/null
+++ b/Test/server/simple-session.transcript
@@ -0,0 +1,637 @@
+# RUN: "%server" "%s" > "%t"
+# RUN: %diff "%s.expect" "%t"
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG4gfVxuIiwi
+c291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG4iLCJzb3VyY2VJc0ZpbGUiOmZh
+bHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7Iiwic291
+cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gICIs
+InNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG59Iiwi
+c291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG5cbn0i
+LCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIFxu
+fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHhc
+bn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIFxu
+fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+clxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+ciB4IDo9IDE7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+ciB4IDo9IDE7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDI7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDI7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFs
+c2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKCkg
+e1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJzb3VyY2VJc0Zp
+bGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKCkg
+e1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJzb3VyY2VJc0Zp
+bGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcblxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcblxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxufSIs
+InNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxu
+fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxu
+fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgXG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzXG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvclxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBcbn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBpbnQsIHgnICogeCcgPiAwO1xufSIsInNvdXJj
+ZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBpbnQsIHgnICogeCcgPiAwO1xufSIsInNvdXJj
+ZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4J2ludCwgeCcgKiB4JyA+IDA7XG59Iiwic291cmNlSXNG
+aWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50LCB4JyAqIHgnID4gMDtcbn0iLCJzb3VyY2VJ
+c0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6ICwgeCcgKiB4JyA+IDA7XG59Iiwic291
+cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPiAwO1xufSIsInNvdXJj
+ZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbn0iLCJzb3Vy
+Y2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgXG59Iiwi
+c291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzXG59
+Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn0iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn0iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cbiIs
+InNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNl
+fQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTScodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg
+eCAqIHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0odDogbmF0KVxuICByZXF1aXJlcyB0
+ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBhc3NlcnQgZm9y
+YWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQgeCAqIHggPiAwO1xufVxuXG5z
+dGF0aWMgbWV0aG9kIE0odDogbmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAx
+O1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4
+JyA+PSAwO1xuICBhc3NlcnQgeCAqIHggPiAwO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0odDogbmF0
+KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAz
+O1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQgeCAq
+IHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg
+eCAqIHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg
+eCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnID49IDA7XG4gIGFzc2Vy
+dCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnICAwO1xuICBhc3NlcnQg
+eCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDwgMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc2Vy
+dCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIFxuICBh
+c3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc1xu
+ICBhc3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc2Vy
+XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc1xu
+ICBhc3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbHNlO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbHNlO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect
new file mode 100644
index 00000000..a5f841bc
--- /dev/null
+++ b/Test/server/simple-session.transcript.expect
@@ -0,0 +1,992 @@
+# Reading from simple-session.transcript
+
+Verifying CheckWellformed$$_module.__default.A ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+  [2 proof obligations]  error
+transcript(3,9): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [2 proof obligations]  error
+transcript(3,9): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [2 proof obligations]  error
+transcript(3,9): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [2 proof obligations]  error
+transcript(3,9): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+
+Verifying CheckWellformed$$_module.__default.A ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+  [0 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,13): Error: rbrace expected
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(6,2): Error: rbrace expected
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+  [0 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [0 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [0 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(7,0): Error: invalid UpdateStmt
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [0 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(7,0): Error: invalid VarDeclStatement
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+  [1 proof obligation]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+  [2 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [2 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [2 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+  [3 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [3 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [3 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(6,2): Error: EOF expected
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(6,2): Error: EOF expected
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+  [3 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(11,0): Error: invalid UpdateStmt
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(11,0): Error: semi expected
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(11,0): Error: invalid UnaryExpression
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,25): Error: openparen expected
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,25): Error: openparen expected
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,26): Error: invalid QSep
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,28): Error: invalid QSep
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,27): Error: invalid UnaryExpression
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+  [1 proof obligation]  error
+transcript(10,9): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+  [1 proof obligation]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(12,0): Error: invalid UpdateStmt
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+  [1 proof obligation]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,14): Error: Duplicate member name: M'
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,14): Error: Duplicate member name: M'
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,14): Error: Duplicate member name: M'
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,14): Error: Duplicate member name: M'
+transcript(24,14): Error: Duplicate member name: M'
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,14): Error: Duplicate member name: M'
+transcript(24,14): Error: Duplicate member name: M'
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,14): Error: Duplicate member name: M'
+transcript(24,14): Error: Duplicate member name: M'
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,14): Error: Duplicate member name: M'
+transcript(24,14): Error: Duplicate member name: M'
+transcript(33,14): Error: Duplicate member name: M'
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,14): Error: Duplicate member name: M
+transcript(33,14): Error: Duplicate member name: M
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M0 ...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M1 ...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M2 ...
+  [5 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M2 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M2...
+  [5 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M2 ...
+  [2 proof obligations]  error
+transcript(38,9): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(38,38): Error: semi expected
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M2 ...
+  [2 proof obligations]  error
+transcript(38,9): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M2 ...
+  [2 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M2 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M2...
+  [2 proof obligations]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(40,2): Error: invalid UpdateStmt
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(40,2): Error: invalid UpdateStmt
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(40,2): Error: invalid UpdateStmt
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M2 ...
+  [1 proof obligation]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(40,9): Error: invalid AssertStmt
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(40,9): Error: invalid AssertStmt
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(40,9): Error: unresolved identifier: fal
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M2 ...
+  [1 proof obligation]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+  [5 proof obligations]  verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2...
+  [0 proof obligations]  verified
+
+Verifying Impl$$_module.__default.M2 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M2...
+  [1 proof obligation]  verified
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]