Add test for issue #5647

dafny-lang · Aug 5, 2024 · b9757ff · b9757ff
1 parent b1aa83d
commit b9757ff
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 0 deletions.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5647.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5647.dfy
@@ -0,0 +1,13 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+function method {:tailrecursion} GetMaps(
+    opts : string,
+    shortMap : map<char, string> := map[])
+    : map<char, string> 
+  {
+    if |opts| == 0 then
+      shortMap
+    else
+      var shortMap := shortMap[opts[0] := "spoo"];
+      GetMaps(opts[1..], shortMap)
+  }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5647.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5647.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with TODO verified, TODO errors