Updated test output

Author: Rustan Leino

Test/server/simple-session.transcript.expect

@@ -9,23 +9,26 @@ Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
 
 Verifying Impl$$_module.__default.A ...
-  [1 proof obligation]  error
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  error
 transcript(3,9): Error: assertion violation
 Execution trace:
     (0,0): anon0
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
 
 Verifying Impl$$_module.__default.A ...
-  [1 proof obligation]  error
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  error
 transcript(3,9): Error: assertion violation
 Execution trace:
     (0,0): anon0
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
 
 Verifying Impl$$_module.__default.A ...
-  [1 proof obligation]  error
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+  [0 proof obligations]  error
 transcript(3,9): Error: assertion violation
 Execution trace:
     (0,0): anon0
@@ -146,6 +149,7 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 transcript(10,9): Warning: /!\ No terms found to trigger on.
 
 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]]
@@ -157,14 +161,15 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 transcript(10,9): Warning: /!\ No terms found to trigger on.
 
 Verifying Impl$$_module.__default.M_k ...
-  [2 proof obligations]  verified
+  [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 Impl$$_module.__default.M_k ...
-  [2 proof obligations]  verified
+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
@@ -230,7 +235,8 @@ transcript(29,9): Warning: /!\ No terms found to trigger on.
 transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying Impl$$_module.__default.M_k ...
-  [2 proof obligations]  verified
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
 
 Verifying Impl$$_module.__default.M0 ...
   [2 proof obligations]  verified
@@ -252,15 +258,19 @@ transcript(29,9): Warning: /!\ No terms found to trigger on.
 transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying Impl$$_module.__default.M_k ...
-  [2 proof obligations]  verified
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
 
 Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
   [2 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]]
@@ -274,12 +284,15 @@ transcript(29,9): Warning: /!\ No terms found to trigger on.
 transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying Impl$$_module.__default.M_k ...
-  [2 proof obligations]  verified
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
 
 Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M2 ...
@@ -306,12 +319,15 @@ transcript(29,9): Warning: /!\ No terms found to trigger on.
 transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying Impl$$_module.__default.M_k ...
-  [2 proof obligations]  verified
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
 
 Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M2 ...
@@ -331,12 +347,15 @@ transcript(29,9): Warning: /!\ No terms found to trigger on.
 transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying Impl$$_module.__default.M_k ...
-  [2 proof obligations]  verified
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
 
 Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M2 ...
@@ -353,15 +372,19 @@ transcript(29,9): Warning: /!\ No terms found to trigger on.
 transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying Impl$$_module.__default.M_k ...
-  [2 proof obligations]  verified
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
 
 Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
   [2 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]]
@@ -396,16 +419,19 @@ transcript(29,9): Warning: /!\ No terms found to trigger on.
 transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying Impl$$_module.__default.M_k ...
-  [2 proof obligations]  verified
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
 
 Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M2 ...
-  [2 proof obligations]  verified
+  [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
@@ -439,16 +465,19 @@ transcript(29,9): Warning: /!\ No terms found to trigger on.
 transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying Impl$$_module.__default.M_k ...
-  [2 proof obligations]  verified
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
 
 Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M2 ...
-  [2 proof obligations]  verified
+  [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
@@ -461,16 +490,20 @@ transcript(29,9): Warning: /!\ No terms found to trigger on.
 transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying Impl$$_module.__default.M_k ...
-  [2 proof obligations]  verified
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+  [1 proof obligation]  verified
 
 Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
   [2 proof obligations]  verified
 
 Verifying Impl$$_module.__default.M2 ...
-  [2 proof obligations]  verified
+Retrieving cached verification result for implementation Impl$$_module.__default.M2...
+  [1 proof obligation]  verified
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
 Verification completed successfully!