Merge

8 files changed, 730 insertions, 29 deletions

diff --git a/Test/dafny0/SeqFromArray.dfy.expect b/Test/dafny0/SeqFromArray.dfy.expect
index af845d3e..5395e298 100644
--- a/Test/dafny0/SeqFromArray.dfy.expect
+++ b/Test/dafny0/SeqFromArray.dfy.expect
@@ -1,3 +1,6 @@
+SeqFromArray.dfy(56,13): Warning: (!) No terms found to trigger on.

+SeqFromArray.dfy(76,17): Warning: (!) No terms found to trigger on.

+SeqFromArray.dfy(82,17): Warning: (!) No terms found to trigger on.

 

 Dafny program verifier finished with 10 verified, 0 errors

 Program compiled successfully

diff --git a/Test/dafny0/TriggerInPredicate.dfy b/Test/dafny0/TriggerInPredicate.dfy
index 3f2eac2c..b9c372dc 100644
--- a/Test/dafny0/TriggerInPredicate.dfy
+++ b/Test/dafny0/TriggerInPredicate.dfy
@@ -3,7 +3,7 @@
 

 predicate A(x: bool, y: bool) { x }

 

-predicate B(x: bool, z: bool) { forall y {:trigger A(x, y) } :: A(x, y) && z }

+predicate B(x: bool, z: bool) { forall y {:trigger A(x, y)} :: A(x, y) && z }

 

 // Inlining is disabled here to prevent pollution of the trigger in B

 method C() requires B(true || false, true) {}

diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect
index 7f6e0268..1cbd4034 100644
--- a/Test/dafny0/TriggerInPredicate.dfy.expect
+++ b/Test/dafny0/TriggerInPredicate.dfy.expect
@@ -1,3 +1,5 @@
+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {A(x, y)}.

+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {z}.

 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.

 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.

 

diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg
index c5718f86..2d57d389 100644
--- a/Test/lit.site.cfg
+++ b/Test/lit.site.cfg
@@ -22,7 +22,7 @@ config.suffixes = ['.dfy']
 # excludes: A list of directories to exclude from the testsuite. The 'Inputs'
 # subdirectories contain auxiliary inputs for various tests in their parent
 # directories.
-config.excludes = ['Inputs']
+config.excludes = ['Inputs', 'sandbox']
 
 # test_source_root: The root path where tests are located.
 config.test_source_root = os.path.dirname(os.path.abspath(__file__))
diff --git a/Test/runTests.py b/Test/runTests.py
index ebdb0655..7cd90454 100644
--- a/Test/runTests.py
+++ b/Test/runTests.py
@@ -6,6 +6,7 @@ import shutil
 import argparse

 import operator

 import platform

+from math import floor, ceil

 from enum import Enum

 from time import time, strftime

 from collections import defaultdict

@@ -147,12 +148,12 @@ class Test:
 

     @staticmethod

     def build_report(tests, name):

-        time = strftime("%Y-%m-%d-%H-%M-%S")

+        now = strftime("%Y-%m-%d-%H-%M-%S")

         if name:

             directory, fname = os.path.split(name)

-            name = os.path.join(directory, time + "--" + fname)

+            name = os.path.join(directory, now + "--" + fname)

         else:

-            name = time

+            name = now

 

         with open(name + ".csv", mode='w', newline='') as writer:

             csv_writer = csv.DictWriter(writer, Test.COLUMNS, dialect='excel')

@@ -169,6 +170,25 @@ class Test:
         return results

 

     @staticmethod

+    def mean_duration(results, margin):

+        durations = sorted(result.duration for result in results

+                           if result.status in (TestStatus.PASSED, TestStatus.FAILED))

+        if len(durations) >= 15:

+            lq = durations[floor(0.25 * len(durations))]

+            hq = durations[ceil(0.85 * len(durations))]

+            iqr = hq - lq

+            filtered = [d for d in durations if (lq - margin * iqr) <= d <= (hq + margin * iqr)]

+            if filtered:

+                avg = sum(durations) / len(durations)

+                trimmed_avg = sum(filtered) / len(filtered)

+                outliers_count = len(durations) - len(filtered)

+                msg = "mean completion time: {:.2f}s".format(avg)

+                if outliers_count > 0:

+                    msg += "; ignoring {} outliers: {:.2f}s".format(outliers_count, trimmed_avg)

+                return " ({})".format(msg)

+        return ""

+

+    @staticmethod

     def summarize(results):

         debug(Debug.INFO, "\nTesting complete ({} test(s))".format(len(results)))

 

@@ -193,7 +213,8 @@ class Test:
                         writer.write("{}\n".format(t.name))

                 debug(Debug.REPORT, "Some tests failed: use [runTests.py failing.lst] to rerun the failing tests")

 

-            debug(Debug.REPORT, "Testing took {:.2f}s on {} thread(s)".format(results[0].suite_time, results[0].njobs))

+            debug(Debug.REPORT, "Testing took {:.2f}s on {} thread(s){}".format(

+                results[0].suite_time, results[0].njobs, Test.mean_duration(results, 1.5)))

 

 

     def run(self):

@@ -231,7 +252,7 @@ class Test:
                 with open(self.temp_output_path, mode='ab') as writer:

                     writer.write(stdout + stderr)

             if stderr != b"":

-                debug(Debug.TRACE, stderr)

+                debug(Debug.TRACE, stderr.decode("utf-8"))

 

             self.update_status()

         except TimeoutExpired:

@@ -470,12 +491,13 @@ def run_tests(args):
         debug(Debug.ERROR, "Testing interrupted")

 

 

-def diff(paths, accept, difftool):

+def diff(paths, force_accept, difftool):

     for path in expand_lsts(paths):

         if not os.path.exists(path):

             debug(Debug.ERROR, "Not found: {}".format(path))

         else:

             test = Test(None, path, [], None)

+            accept = force_accept

 

             if not accept:

                 call([difftool, test.expect_path, test.temp_output_path])

diff --git a/Test/server/minimal.transcript b/Test/server/minimal.transcript
new file mode 100644
index 00000000..9625fb00
--- /dev/null
+++ b/Test/server/minimal.transcript
@@ -0,0 +1,8 @@
+# RUN: %server "%s" > "%t"

+# RUN: %diff "%s.expect" "%t"

+verify

+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp

+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50

+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz

+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==

+[[DAFNY-CLIENT: EOM]]

diff --git a/Test/server/minimal.transcript.expect b/Test/server/minimal.transcript.expect
new file mode 100644
index 00000000..bf3f9dfb
--- /dev/null
+++ b/Test/server/minimal.transcript.expect
@@ -0,0 +1,14 @@
+# Reading from minimal.transcript

+

+Verifying CheckWellformed$$_module.__default.A ...

+  [0 proof obligations]  verified

+

+Verifying Impl$$_module.__default.A ...

+  [2 proof obligations]  error

+transcript(3,9): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
diff --git a/Test/server/simple-session.transcript.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!