From 22e292faf973ee8c42af31ab4719ac14321ef4a9 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 9 Aug 2023 09:03:11 -0700
Subject: [PATCH] Include the solver used in each VCResult

---
 Source/VCGeneration/Split.cs    | 4 +++-
 Source/VCGeneration/VCResult.cs | 4 +++-
 2 files changed, 6 insertions(+), 2 deletions(-)

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<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
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<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) {