Include the solver used in each VCResult

boogie-org · Aug 9, 2023 · 22e292f · 22e292f
1 parent 0b1e684
commit 22e292f
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git 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<Block> 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
@@ -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<Counterexample> counterExamples,
     List<AssertCmd> asserts,
     IEnumerable<string> coveredElements,
-    int resourceCount
+    int resourceCount,
+    SolverKind? solverUsed
   ) {
     public void ComputePerAssertOutcomes(out Dictionary<AssertCmd, ProverInterface.Outcome> perAssertOutcome,
       out Dictionary<AssertCmd, Counterexample> perAssertCounterExamples) {