1 files changed, 673 insertions, 21 deletions
diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect
index 89c3351d..91429d8e 100644
--- a/Test/server/simple-session.transcript.expect
+++ b/Test/server/simple-session.transcript.expect
@@ -1,24 +1,60 @@
 # 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
@@ -27,22 +63,114 @@ Verification completed successfully!
 transcript(6,2): Error: rbrace expected
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
-Verification completed successfully!
-[SUCCESS] [[DAFNY-SERVER: EOM]]
-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: ident expected
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
-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
@@ -51,21 +179,113 @@ Verification completed successfully!
 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]]
-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
-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
-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
-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
-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 ...
+  [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
@@ -77,6 +297,20 @@ 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
@@ -112,15 +346,59 @@ 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
+
+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
+
+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
+
+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
@@ -128,9 +406,39 @@ 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
+
+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
+
+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
@@ -190,18 +498,130 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 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
+
+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
+
+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
+
+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
@@ -218,6 +638,44 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 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
+
+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
@@ -227,12 +685,90 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 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
+
+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
+
+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
@@ -260,6 +796,44 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 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
+
+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
@@ -287,12 +861,90 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 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
+
+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
+
+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!