Merge branch 'master' into coverage-trace

boogie-org · Aug 11, 2023 · b9c7778 · b9c7778
2 parents 40d1e08 + 50a4d5b
commit b9c7778
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) {