diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index b9c97ffa6..14db25dec 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -8,6 +8,7 @@ using System.IO; using Microsoft.BaseTypes; using Microsoft.Boogie.VCExprAST; +using Microsoft.Boogie.SMTLib; namespace VC { @@ -1287,7 +1288,8 @@ public int GetHashCode(List obj) counterExamples: Counterexamples, asserts: Asserts, coveredElements: CoveredElements, - resourceCount: resourceCount); + resourceCount: resourceCount, + solverUsed: (options as SMTLibSolverOptions)?.Solver); callback.OnVCResult(result); if (options.VcsDumpSplits) diff --git a/Source/VCGeneration/VCResult.cs b/Source/VCGeneration/VCResult.cs index 982209ec3..a3b8956f5 100644 --- a/Source/VCGeneration/VCResult.cs +++ b/Source/VCGeneration/VCResult.cs @@ -8,6 +8,7 @@ using System.IO; using Microsoft.BaseTypes; using Microsoft.Boogie.VCExprAST; +using Microsoft.Boogie.SMTLib; namespace VC { @@ -25,7 +26,8 @@ public record VCResult List counterExamples, List asserts, IEnumerable coveredElements, - int resourceCount + int resourceCount, + SolverKind? solverUsed ) { public void ComputePerAssertOutcomes(out Dictionary perAssertOutcome, out Dictionary perAssertCounterExamples) {