From 5bd920307ae28e820c379e8678c32bd9cdd871cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <MikaelMayer@users.noreply.github.com>
Date: Thu, 26 Jan 2023 12:58:47 -0600
Subject: [PATCH] Test if this is a typo in prelude (#3412)

This PR fixes #3411
Seems like one of Boogie's axiom was wrong, but it was unnoticed because
another application axiom was ignoring the wrong argument.
I added the test case of the issue.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
---
 Source/DafnyCore/DafnyPrelude.bpl         | 2 +-
 Test/git-issues/git-issue-3411.dfy        | 7 +++++++
 Test/git-issues/git-issue-3411.dfy.expect | 2 ++
 docs/dev/news/3411.fix                    | 1 +
 4 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 Test/git-issues/git-issue-3411.dfy
 create mode 100644 Test/git-issues/git-issue-3411.dfy.expect
 create mode 100644 docs/dev/news/3411.fix

diff --git a/Source/DafnyCore/DafnyPrelude.bpl b/Source/DafnyCore/DafnyPrelude.bpl
index f2dc3b6879d..d6aef7285ef 100644
--- a/Source/DafnyCore/DafnyPrelude.bpl
+++ b/Source/DafnyCore/DafnyPrelude.bpl
@@ -1018,7 +1018,7 @@ axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType ::
 axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType, i: int ::
   { Seq#Index(Seq#Create(ty, heap, len, init), i) }
   $IsGoodHeap(heap) && 0 <= i && i < len ==>
-  Seq#Index(Seq#Create(ty, heap, len, init), i) == Apply1(TInt, TSeq(ty), heap, init, $Box(i)));
+  Seq#Index(Seq#Create(ty, heap, len, init), i) == Apply1(TInt, ty, heap, init, $Box(i)));
 
 function Seq#Append<T>(Seq T, Seq T): Seq T;
 axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }
diff --git a/Test/git-issues/git-issue-3411.dfy b/Test/git-issues/git-issue-3411.dfy
new file mode 100644
index 00000000000..c9c95d4c83d
--- /dev/null
+++ b/Test/git-issues/git-issue-3411.dfy
@@ -0,0 +1,7 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Test(f: int -> int) {
+  assert seq(1, x => f(x))[0] == f(0);  // No problem
+  assert seq(1, f)[0] == f(0);  // No problem anymore
+}
\ No newline at end of file
diff --git a/Test/git-issues/git-issue-3411.dfy.expect b/Test/git-issues/git-issue-3411.dfy.expect
new file mode 100644
index 00000000000..823a60a105c
--- /dev/null
+++ b/Test/git-issues/git-issue-3411.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
diff --git a/docs/dev/news/3411.fix b/docs/dev/news/3411.fix
new file mode 100644
index 00000000000..1207ee55fbe
--- /dev/null
+++ b/docs/dev/news/3411.fix
@@ -0,0 +1 @@
+Fixed an axiom related to sequence comprehension extraction
\ No newline at end of file