diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index c4b05087e..dcfd753f4 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -1182,10 +1182,6 @@ public static IEnumerable FindReachableNodesInGraphWithMergeNodes( continue; } - if (visit != null && visit(node) == false) - { - continue; - } if (node is IEnumerable objects) { if (!visitedEdges.IsSupersetOf(objects)) { @@ -1193,6 +1189,10 @@ public static IEnumerable FindReachableNodesInGraphWithMergeNodes( } } visitedEdges.Add(node); + if (visit != null && visit(node) == false) + { + continue; + } var outgoing = edges.GetValueOrDefault(node) ?? new List(); foreach (var x in outgoing) diff --git a/Source/VCGeneration/Prune/Prune.cs b/Source/VCGeneration/Prune/Prune.cs index 7aa2ed1cd..11c851024 100644 --- a/Source/VCGeneration/Prune/Prune.cs +++ b/Source/VCGeneration/Prune/Prune.cs @@ -67,21 +67,18 @@ public static IEnumerable GetLiveDeclarations(VCGenOptions options, blocksVisitor.Visit(block); } - var revealedOutgoing = options.Prune == PruneMode.AllRevealed - ? blocksVisitor.Outgoing - : blocksVisitor.Outgoing.Where(d => - DeclarationFilter(d)); - var keepRoots = program.TopLevelDeclarations.Where(d => QKeyValue.FindBoolAttribute(d.Attributes, "keep")); var reachableDeclarations = GraphAlgorithms.FindReachableNodesInGraphWithMergeNodes(program.DeclarationDependencies, - revealedOutgoing.Concat(keepRoots).ToHashSet(), - node => node is not Function function || blocksVisitor.RevealedFunctions.Contains(function)) - .OfType().Where(d => DeclarationFilter(d)).ToHashSet(); + blocksVisitor.Outgoing.Concat(keepRoots).ToHashSet(), DeclarationFilter).ToHashSet(); return program.TopLevelDeclarations.Where(d => d is not Constant && d is not Axiom && d is not Function || reachableDeclarations.Contains(d)); - bool DeclarationFilter(Declaration d) + bool DeclarationFilter(object d) { + if (options.Prune != PruneMode.ExplicitReveal) + { + return true; + } return d is not Function function || blocksVisitor.RevealedFunctions.Contains(function); } }