Test

dafny-lang · Oct 11, 2024 · a4da0f3 · a4da0f3
1 parent c3dc53f
commit a4da0f3
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-5814.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-5814.dfy
@@ -0,0 +1,18 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+trait MyTrait<T> {
+ method Bar(ghost x: T, y: T) returns (z: T)
+}
+
+class MyClass extends MyTrait<int> {
+ constructor() {}
+ method Bar(ghost x: int, y: int) returns (z: int) {
+ return y;
+ }
+}
+
+method Main() {
+ var c := new MyClass();
+ var z := c.Bar(7, 42);
+ expect z == 42;
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-5814.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-5814.dfy.expect