From d316c50e0bf7ae90b2a97b4e2da619b336d94369 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Thu, 22 Jun 2023 10:21:39 -0500
Subject: [PATCH] Add test for issue #4205

---
 Test/git-issues/git-issue-4205.dfy        | 12 ++++++++++++
 Test/git-issues/git-issue-4205.dfy.expect |  2 ++
 2 files changed, 14 insertions(+)
 create mode 100644 Test/git-issues/git-issue-4205.dfy
 create mode 100644 Test/git-issues/git-issue-4205.dfy.expect

diff --git a/Test/git-issues/git-issue-4205.dfy b/Test/git-issues/git-issue-4205.dfy
new file mode 100644
index 00000000000..ef8bc224b17
--- /dev/null
+++ b/Test/git-issues/git-issue-4205.dfy
@@ -0,0 +1,12 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T {
+  opaque function bar(): int
+}
+
+class F extends T {
+  opaque function bar(): int {
+    1
+  }
+}
\ No newline at end of file
diff --git a/Test/git-issues/git-issue-4205.dfy.expect b/Test/git-issues/git-issue-4205.dfy.expect
new file mode 100644
index 00000000000..0f497be06d5
--- /dev/null
+++ b/Test/git-issues/git-issue-4205.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with TODO verified, TODO errors