expose PrunedDeclarations

boogie-org · Oct 3, 2024 · 4d2b065 · 4d2b065
1 parent 4efba3d
commit 4d2b065
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs
@@ -899,7 +899,9 @@ public VerificationRunResult ReadOutcome(int iteration, Checker checker, Verifie
           Asserts: Asserts,
           CoveredElements: CoveredElements,
           ResourceCount: resourceCount,
-          SolverUsed: (Options as SMTLibSolverOptions)?.Solver);
+          SolverUsed: (Options as SMTLibSolverOptions)?.Solver,
+          PrunedDeclarations: PrunedDeclarations
+          );
         callback.OnVCResult(result);
 
         if (Options.VcsDumpSplits)

diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs
@@ -18,7 +18,8 @@ public record VerificationRunResult
     List<AssertCmd> Asserts,
     IEnumerable<TrackedNodeComponent> CoveredElements,
     int ResourceCount,
-    SolverKind? SolverUsed
+    SolverKind? SolverUsed,
+    IReadOnlyList<Declaration> PrunedDeclarations
   ) {
     public void ComputePerAssertOutcomes(out Dictionary<AssertCmd, SolverOutcome> perAssertOutcome,
       out Dictionary<AssertCmd, Counterexample> perAssertCounterExamples) {