Add test for multiple let bindings

Also bump version of lean and lean-auto
boogie-org · Nov 13, 2024 · 8629183 · 8629183
1 parent c8cf4e0
commit 8629183
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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;
+}