summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks/AnswerRuntimeChecking
diff options
context:
space:
mode:
Diffstat (limited to 'Test/VSI-Benchmarks/AnswerRuntimeChecking')
-rw-r--r--Test/VSI-Benchmarks/AnswerRuntimeChecking9
1 files changed, 0 insertions, 9 deletions
diff --git a/Test/VSI-Benchmarks/AnswerRuntimeChecking b/Test/VSI-Benchmarks/AnswerRuntimeChecking
index 841a04cf..49a440db 100644
--- a/Test/VSI-Benchmarks/AnswerRuntimeChecking
+++ b/Test/VSI-Benchmarks/AnswerRuntimeChecking
@@ -1,29 +1,20 @@
-------------------- b1 --------------------
-
-Dafny program verifier finished with 10 verified, 0 errors
Compiled assembly into b1.exe
Rewrote assembly into b1.exe
-------------------- b3 --------------------
-b3.dfy(114,28): Error BP5005: This loop invariant might not be maintained by the loop.
-
-Dafny program verifier finished with 9 verified, 1 error
Compilation error: Method _default.Queue.Init has no body
Compilation error: Method _default.Queue.Enqueue has no body
Compilation error: Method _default.Queue.Dequeue has no body
-------------------- b7 --------------------
-
-Dafny program verifier finished with 23 verified, 0 errors
Compilation error: Method _default.Queue.Init has no body
Compilation error: Method _default.Queue.Enqueue has no body
Compilation error: Method _default.Queue.Dequeue has no body
Compilation error: Method _default.Client.Sort has no body
-------------------- b8 --------------------
-
-Dafny program verifier finished with 42 verified, 0 errors
Compilation error: Method _default.Queue.Init has no body
Compilation error: Method _default.Queue.Enqueue has no body
Compilation error: Method _default.Queue.Dequeue has no body