Allow goto to have no targets

boogie-org · Mar 19, 2024 · 29979dc · 29979dc
1 parent 4cc7547
commit 29979dc
Showing 1 changed file with 7 additions and 3 deletions.
diff --git 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;
   }