1 files changed, 992 insertions, 0 deletions
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]]