Fixes

boogie-org · Nov 22, 2024 · c9207aa · c9207aa
1 parent dc86662
commit c9207aa
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 9 deletions.
diff --git a/Source/Provers/LeanAuto/LeanAutoGenerator.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs
@@ -48,7 +48,7 @@ public static void EmitPassiveProgramAsLean(VCGenOptions options, Program p, Tex
       var liveDeclarations =
         !options.Prune
           ? p.TopLevelDeclarations
-          : Pruner.GetLiveDeclarations(options, p, allBlocks.ToList()).ToList();
+          : Pruner.GetLiveDeclarations(options, p, allBlocks.ToList()).LiveDeclarations.ToList();
 
       generator.WriteLine("-- Type constructors");
       // Always include all type constructors

diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs
@@ -28,22 +28,34 @@ public class Split : ProofRun
       readonly List<Block> bigBlocks = new();
       public List<AssertCmd> Asserts => Blocks.SelectMany(block => block.Cmds.OfType<AssertCmd>()).ToList();
       private IReadOnlyList<Declaration> prunedDeclarations;
-      public ISet<Function> HiddenFunctions;
-
+
+      public ISet<Function> HiddenFunctions {
+        get {
+          if (hiddenFunctions == null) {
+            ComputePrunedDeclsAndHiddenFunctions();
+          }
+          return hiddenFunctions;
+        }
+      }
+
       public IReadOnlyList<Declaration> PrunedDeclarations {
         get {
-          if (prunedDeclarations == null)
-          {
-            var (liveDeclarations, hiddenFunctions) =
-              Pruner.GetLiveDeclarations(parent.Options, parent.program, Blocks);
-            HiddenFunctions = hiddenFunctions;
-            prunedDeclarations = liveDeclarations.ToList();
+          if (prunedDeclarations == null) {
+            ComputePrunedDeclsAndHiddenFunctions();
           }
 
           return prunedDeclarations;
         }
       }
 
+      private void ComputePrunedDeclsAndHiddenFunctions()
+      {
+        var (liveDeclarations, hiddenFunctions) =
+          Pruner.GetLiveDeclarations(parent.Options, parent.program, Blocks);
+        this.hiddenFunctions = hiddenFunctions;
+        prunedDeclarations = liveDeclarations.ToList();
+      }
+
       readonly Dictionary<Block /*!*/, BlockStats /*!*/> /*!*/
         stats = new Dictionary<Block /*!*/, BlockStats /*!*/>();
 
@@ -204,6 +216,7 @@ public void DumpDot(int splitNum)
 
       int bsid;
       private readonly Func<IList<Block>> getBlocks;
+      private ISet<Function> hiddenFunctions;
 
       BlockStats GetBlockStats(Block b)
       {