diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 7cf747118..f063c2215 100644 --- 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 index b2566f93e..89d511672 100644 --- a/Source/VCGeneration/VerificationRunResult.cs +++ b/Source/VCGeneration/VerificationRunResult.cs @@ -18,7 +18,8 @@ public record VerificationRunResult List Asserts, IEnumerable CoveredElements, int ResourceCount, - SolverKind? SolverUsed + SolverKind? SolverUsed, + IReadOnlyList PrunedDeclarations ) { public void ComputePerAssertOutcomes(out Dictionary perAssertOutcome, out Dictionary perAssertCounterExamples) {