From 29979dc812de2c8d19edc426c455b87b7c105d98 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Tue, 19 Mar 2024 13:59:50 -0700
Subject: [PATCH] Allow `goto` to have no targets

---
 Source/Provers/LeanAuto/LeanAutoGenerator.cs | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/Source/Provers/LeanAuto/LeanAutoGenerator.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs
index cb09966c4..bd9712afb 100644
--- a/Source/Provers/LeanAuto/LeanAutoGenerator.cs
+++ b/Source/Provers/LeanAuto/LeanAutoGenerator.cs
@@ -197,9 +197,13 @@ public override Cmd VisitAssumeCmd(AssumeCmd node)
 
   public override GotoCmd VisitGotoCmd(GotoCmd node)
   {
-    var gotoText = node.labelTargets.Select(l =>
-      $"goto {BlockName(l)}").Aggregate((a, b) => $"{a} {AndString} {b}");
-    Indent(2, gotoText);
+    string cmd = node.labelTargets.Any()
+      ? node
+        .labelTargets
+        .Select(l => $"goto {BlockName(l)}")
+        .Aggregate((a, b) => $"{a} {AndString} {b}")
+      : "ret";
+    Indent(2, cmd);
     return node;
   }