From 8629183289e50a8b9c84f5192c05bacee90a6f87 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 13 Nov 2024 13:54:20 -0800
Subject: [PATCH] Add test for multiple let bindings

Also bump version of lean and lean-auto
---
 Test/lean-auto/lakefile.lean  | 2 +-
 Test/lean-auto/lean-toolchain | 2 +-
 Test/lean-auto/multi-let.bpl  | 9 +++++++++
 3 files changed, 11 insertions(+), 2 deletions(-)
 create mode 100644 Test/lean-auto/multi-let.bpl

diff --git a/Test/lean-auto/lakefile.lean b/Test/lean-auto/lakefile.lean
index 8d422d5e3..ae3b2c2d0 100644
--- a/Test/lean-auto/lakefile.lean
+++ b/Test/lean-auto/lakefile.lean
@@ -6,7 +6,7 @@ package «test» {
 }
 
 require auto from git
-  "https://github.com/leanprover-community/lean-auto"@"0831a6eff8cbb456e90c616bd2f4db51aefea3d0"
+  "https://github.com/leanprover-community/lean-auto"@"60e546ca7a9d40d508e58847a9d0630406835178"
 
 @[default_target]
 lean_lib «ToBuild» {
diff --git a/Test/lean-auto/lean-toolchain b/Test/lean-auto/lean-toolchain
index 4ef27c472..5a9c76dc9 100644
--- a/Test/lean-auto/lean-toolchain
+++ b/Test/lean-auto/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.11.0
diff --git a/Test/lean-auto/multi-let.bpl b/Test/lean-auto/multi-let.bpl
new file mode 100644
index 000000000..841e5e761
--- /dev/null
+++ b/Test/lean-auto/multi-let.bpl
@@ -0,0 +1,9 @@
+procedure P(x: int, y: int) {
+    var z: int;
+    var w: int;
+
+    z := (var a, b := x+1, y+1; a);
+    w := (var a, b := x+1, y+1; b);
+    assert (z - 1) == x;
+    assert (w - 1) == y;
+}