diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 467cca178..127763000 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -19,7 +19,7 @@
 
 namespace Microsoft.Boogie
 {
-  public record ProcessedProgram(Program Program, Action<VCGen, Implementation, ImplementationRunResult> PostProcessResult) {
+  public record ProcessedProgram(Program Program, Action<VerificationConditionGenerator, Implementation, ImplementationRunResult> PostProcessResult) {
     public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) {
     }
   }
@@ -880,7 +880,7 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc
       var batchCompleted = new Subject<(Split split, VerificationRunResult vcResult)>();
       var completeVerification = largeThreadTaskFactory.StartNew(async () =>
       {
-        var vcgen = new VCGen(processedProgram.Program, checkerPool);
+        var vcgen = new VerificationConditionGenerator(processedProgram.Program, checkerPool);
         vcgen.CachingActionCounts = stats.CachingActionCounts;
         verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;
         verificationResult.Start = DateTime.UtcNow;
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 5883784f9..11a51b434 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -52,7 +52,7 @@ public virtual void UpdateAssignment(Dictionary<Variable, bool> assignment)
     {
     }
 
-    public virtual void UpdateOutcome(Outcome outcome)
+    public virtual void UpdateOutcome(SolverOutcome outcome)
     {
     }
 
@@ -158,7 +158,7 @@ public override void UpdateImplementation(Implementation implementation)
       curImp = implementation;
     }
 
-    public override void UpdateOutcome(Outcome o)
+    public override void UpdateOutcome(SolverOutcome o)
     {
       Contract.Assert(curImp != null);
       DateTime endT = DateTime.UtcNow;
@@ -237,7 +237,7 @@ public override void UpdateAssignment(Dictionary<Variable, bool> assignment)
       wr.Flush();
     }
 
-    public override void UpdateOutcome(Outcome outcome)
+    public override void UpdateOutcome(SolverOutcome outcome)
     {
       wr.WriteLine("analysis outcome :" + outcome);
       wr.Flush();
@@ -335,7 +335,7 @@ protected void NotifyAssignment(Dictionary<Variable, bool> assignment)
       Notify((NotifyDelegate) delegate(HoudiniObserver r) { r.UpdateAssignment(assignment); });
     }
 
-    protected void NotifyOutcome(Outcome outcome)
+    protected void NotifyOutcome(SolverOutcome outcome)
     {
       Notify((NotifyDelegate) delegate(HoudiniObserver r) { r.UpdateOutcome(outcome); });
     }
@@ -393,7 +393,7 @@ public class Houdini : ObservableHoudini
   {
     protected Program program;
     protected HashSet<Variable> houdiniConstants;
-    protected VCGen vcgen;
+    protected VerificationConditionGenerator vcgen;
     protected ProverInterface proverInterface;
     protected Graph<Implementation> callGraph;
     protected HashSet<Implementation> vcgenFailures;
@@ -470,7 +470,7 @@ protected void Initialize(TextWriter traceWriter, Program program, HoudiniSessio
       */
 
       var checkerPool = new CheckerPool(Options);
-      this.vcgen = new VCGen(program, checkerPool);
+      this.vcgen = new VerificationConditionGenerator(program, checkerPool);
       this.proverInterface = ProverInterface.CreateProver(Options, program, Options.ProverLogFilePath,
         Options.ProverLogFileAppend, Options.TimeLimit, taskID: GetTaskID());
 
@@ -837,13 +837,13 @@ protected Dictionary<Variable, bool> BuildAssignment(HashSet<Variable> constants
       return initial;
     }
 
-    private bool IsOutcomeNotHoudini(Outcome outcome, List<Counterexample> errors)
+    private bool IsOutcomeNotHoudini(SolverOutcome outcome, List<Counterexample> errors)
     {
       switch (outcome)
       {
-        case Outcome.Valid:
+        case SolverOutcome.Valid:
           return false;
-        case Outcome.Invalid:
+        case SolverOutcome.Invalid:
           Contract.Assume(errors != null);
           foreach (Counterexample error in errors)
           {
@@ -863,14 +863,14 @@ private bool IsOutcomeNotHoudini(Outcome outcome, List<Counterexample> errors)
     // Return true if there was at least one non-candidate error
     protected bool UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,
       Implementation implementation,
-      Outcome outcome,
+      SolverOutcome outcome,
       List<Counterexample> errors)
     {
       string implName = implementation.Name;
       houdiniOutcome.implementationOutcomes.Remove(implName);
       List<Counterexample> nonCandidateErrors = new List<Counterexample>();
 
-      if (outcome == Outcome.Invalid)
+      if (outcome == SolverOutcome.Invalid)
       {
         foreach (Counterexample error in errors)
         {
@@ -937,7 +937,7 @@ protected void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation)
 
     // Updates the worklist and current assignment
     // @return true if the current function is dequeued
-    protected bool UpdateAssignmentWorkList(Outcome outcome,
+    protected bool UpdateAssignmentWorkList(SolverOutcome outcome,
       List<Counterexample> errors)
     {
       Contract.Assume(currentHoudiniState.Implementation != null);
@@ -945,11 +945,11 @@ protected bool UpdateAssignmentWorkList(Outcome outcome,
 
       switch (outcome)
       {
-        case Outcome.Valid:
+        case SolverOutcome.Valid:
           //yeah, dequeue
           break;
 
-        case Outcome.Invalid:
+        case SolverOutcome.Invalid:
           Contract.Assume(errors != null);
 
           foreach (Counterexample error in errors)
@@ -1489,7 +1489,7 @@ private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error)
       return null;
     }
 
-    private async Task<(Outcome, List<Counterexample> errors)> TryCatchVerify(HoudiniSession session, int stage, IReadOnlyList<int> completedStages)
+    private async Task<(SolverOutcome, List<Counterexample> errors)> TryCatchVerify(HoudiniSession session, int stage, IReadOnlyList<int> completedStages)
     {
       try {
         return await session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), GetErrorLimit());
@@ -1497,7 +1497,7 @@ private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error)
       catch (UnexpectedProverOutputException upo)
       {
         Contract.Assume(upo != null);
-        return (Outcome.Undetermined, null);
+        return (SolverOutcome.Undetermined, null);
       }
 
     }
@@ -1551,7 +1551,7 @@ private async Task HoudiniVerifyCurrent(HoudiniSession session, int stage, IRead
 
         #region Explain Houdini
 
-        if (Options.ExplainHoudini && outcome == Outcome.Invalid)
+        if (Options.ExplainHoudini && outcome == SolverOutcome.Invalid)
         {
           Contract.Assume(errors != null);
           // make a copy of this variable
@@ -1587,7 +1587,7 @@ private async Task HoudiniVerifyCurrent(HoudiniSession session, int stage, IRead
 
         if (UpdateAssignmentWorkList(outcome, errors))
         {
-          if (Options.UseUnsatCoreForContractInfer && outcome == Outcome.Valid)
+          if (Options.UseUnsatCoreForContractInfer && outcome == SolverOutcome.Valid)
           {
             await session.UpdateUnsatCore(proverInterface, currentHoudiniState.Assignment);
           }
@@ -1707,7 +1707,7 @@ public class VCGenOutcome
     public VcOutcome VcOutcome;
     public List<Counterexample> errors;
 
-    public VCGenOutcome(Outcome outcome, List<Counterexample> errors)
+    public VCGenOutcome(SolverOutcome outcome, List<Counterexample> errors)
     {
       this.VcOutcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
       this.errors = errors;
diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs
index e4d0959c5..5c1032115 100644
--- a/Source/Houdini/HoudiniSession.cs
+++ b/Source/Houdini/HoudiniSession.cs
@@ -156,7 +156,7 @@ public bool InUnsatCore(Variable constant)
       return false;
     }
 
-    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program,
+    public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, ProverInterface proverInterface, Program program,
       ImplementationRun run, HoudiniStatistics stats, int taskID = -1)
     {
       var impl = run.Implementation;
@@ -195,7 +195,7 @@ public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterf
         new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false));
       proverInterface.DefineMacro(macro, conjecture);
       conjecture = exprGen.Function(macro);
-      handler = new VCGen.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, impl.debugInfos, collector,
+      handler = new VerificationConditionGenerator.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, impl.debugInfos, collector,
         mvInfo, proverInterface.Context, program, this);
     }
 
@@ -252,7 +252,7 @@ private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary<Variable,
 
     public HoudiniOptions Options => houdini.Options;
 
-    public async Task<(Outcome, List<Counterexample> errors)> Verify(
+    public async Task<(SolverOutcome, List<Counterexample> errors)> Verify(
       ProverInterface proverInterface,
       Dictionary<Variable, bool> assignment,
       int errorLimit)
@@ -393,7 +393,7 @@ public async Task Explain(ProverInterface proverInterface,
       var el = Options.ErrorLimit;
       Options.ErrorLimit = 1;
 
-      var outcome = Outcome.Undetermined;
+      var outcome = SolverOutcome.Undetermined;
 
       do
       {
@@ -402,8 +402,8 @@ public async Task Explain(ProverInterface proverInterface,
           handler, CancellationToken.None);
         hardAssumptions.RemoveAt(hardAssumptions.Count - 1);
 
-        if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory ||
-            outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined)
+        if (outcome == SolverOutcome.TimeOut || outcome == SolverOutcome.OutOfMemory ||
+            outcome == SolverOutcome.OutOfResource || outcome == SolverOutcome.Undetermined)
         {
           break;
         }
@@ -436,8 +436,8 @@ public async Task Explain(ProverInterface proverInterface,
         (outcome, var unsatisfiedSoftAssumptions2) = await proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2,
           handler, CancellationToken.None);
 
-        if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory ||
-            outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined)
+        if (outcome == SolverOutcome.TimeOut || outcome == SolverOutcome.OutOfMemory ||
+            outcome == SolverOutcome.OutOfResource || outcome == SolverOutcome.Undetermined)
         {
           break;
         }
@@ -467,8 +467,8 @@ public async Task Explain(ProverInterface proverInterface,
         }
       } while (false);
 
-      if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory ||
-          outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined)
+      if (outcome == SolverOutcome.TimeOut || outcome == SolverOutcome.OutOfMemory ||
+          outcome == SolverOutcome.OutOfResource || outcome == SolverOutcome.Undetermined)
       {
         Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name,
           "TimeOut", Description);
@@ -515,8 +515,8 @@ public async Task UpdateUnsatCore(ProverInterface proverInterface, Dictionary<Va
         assumptionExprs.Add(exprTranslator.LookupVariable(v));
       }
 
-      (Outcome tmp, var unsatCore) = await proverInterface.CheckAssumptions(assumptionExprs, handler, CancellationToken.None);
-      System.Diagnostics.Debug.Assert(tmp == Outcome.Valid);
+      (SolverOutcome tmp, var unsatCore) = await proverInterface.CheckAssumptions(assumptionExprs, handler, CancellationToken.None);
+      System.Diagnostics.Debug.Assert(tmp == SolverOutcome.Valid);
       unsatCoreSet = new HashSet<Variable>();
       foreach (int i in unsatCore)
       {
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index cad437a24..145010769 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -112,7 +112,7 @@ public virtual int StartingProcId()
       return 0;
     }
 
-    public virtual void OnModel(IList<string> labels, Model model, Outcome proverOutcome)
+    public virtual void OnModel(IList<string> labels, Model model, SolverOutcome proverOutcome)
     {
       Contract.Requires(cce.NonNullElements(labels));
     }
@@ -157,7 +157,7 @@ public virtual Absy Label2Absy(string label)
     }
   }
 
-  public abstract Task<Outcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken);
+  public abstract Task<SolverOutcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken);
 
   public virtual void LogComment(string comment)
   {
@@ -232,13 +232,13 @@ public virtual void Check()
   }
 
   // (check-sat + get-unsat-core + checkOutcome)
-  public virtual Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions, ErrorHandler handler,
+  public virtual Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions, ErrorHandler handler,
     CancellationToken cancellationToken)
   {
     throw new NotImplementedException();
   }
 
-  public virtual Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
+  public virtual Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
     ErrorHandler handler, CancellationToken cancellationToken)
   {
     throw new NotImplementedException();
@@ -295,7 +295,7 @@ public virtual void AssertNamed(VCExpr vc, bool polarity, string name)
   public abstract Task GoBackToIdle();
 }
 
-public enum Outcome
+public enum SolverOutcome
 {
   Valid,
   Invalid,
diff --git a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs b/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
index 9e434d272..8a82a21e9 100644
--- a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
+++ b/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
@@ -62,7 +62,7 @@ public override int FlushAxiomsToTheoremProver()
       return 0;
     }
 
-    public override async Task<Outcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit,
+    public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit,
       CancellationToken cancellationToken)
     {
       currentErrorHandler = handler;
@@ -134,7 +134,7 @@ private Task<IReadOnlyList<SExpr>> SendRequestsAndClose(IReadOnlyList<string> re
       return Process.SendRequestsAndCloseInput(sanitizedRequests, cancellationToken);
     }
 
-    private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
+    private async Task<SolverOutcome> CheckSat(CancellationToken cancellationToken)
     {
       var requests = new List<string>();
       requests.Add("(check-sat)");
@@ -148,7 +148,7 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
       }
 
       if (Process == null || HadErrors) {
-        return Outcome.Undetermined;
+        return SolverOutcome.Undetermined;
       }
 
       try {
@@ -159,7 +159,7 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
         catch (TimeoutException) {
           currentErrorHandler.OnResourceExceeded("hard solver timeout");
           resourceCount = -1;
-          return Outcome.TimeOut;
+          return SolverOutcome.TimeOut;
         }
         var responseStack = new Stack<SExpr>(responses.Reverse());
 
@@ -176,8 +176,8 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
           resourceCount = ParseRCount(rlimitSExp);
 
           // Sometimes Z3 doesn't tell us that it ran out of resources
-          if (result != Outcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) {
-            result = Outcome.OutOfResource;
+          if (result != SolverOutcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) {
+            result = SolverOutcome.OutOfResource;
           }
         }
 
@@ -186,16 +186,16 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
 
         if (options.LibOptions.ProduceUnsatCores) {
           var unsatCoreSExp = responseStack.Pop();
-          if (result == Outcome.Valid) {
+          if (result == SolverOutcome.Valid) {
             ReportCoveredElements(unsatCoreSExp);
           }
         }
 
-        if (result == Outcome.Invalid) {
+        if (result == SolverOutcome.Invalid) {
           var labels = CalculatePath(currentErrorHandler.StartingProcId(), errorModel);
           if (labels.Length == 0) {
             // Without a path to an error, we don't know what to report
-            result = Outcome.Undetermined;
+            result = SolverOutcome.Undetermined;
           } else {
             currentErrorHandler.OnModel(labels, errorModel, result);
           }
@@ -294,13 +294,13 @@ public override Task<List<string>> UnsatCore()
       throw new NotSupportedException("Batch mode solver interface does not support unsat cores.");
     }
 
-    public override Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions,
+    public override Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions,
       ErrorHandler handler, CancellationToken cancellationToken)
     {
       throw new NotSupportedException("Batch mode solver interface does not support checking assumptions.");
     }
 
-    public override Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
+    public override Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
       ErrorHandler handler, CancellationToken cancellationToken)
     {
       throw new NotSupportedException("Batch mode solver interface does not support checking assumptions.");
diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
index 56736194e..71f5ab872 100644
--- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
+++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
@@ -63,7 +63,7 @@ public override int FlushAxiomsToTheoremProver()
     }
 
     private bool hasReset = true;
-    public override async Task<Outcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken)
+    public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken)
     {
       currentErrorHandler = handler;
       try
@@ -185,12 +185,12 @@ public override void FullReset(VCExpressionGenerator generator)
     }
 
     [NoDefaultContract]
-    public async Task<Outcome> CheckSat(CancellationToken cancellationToken,
+    public async Task<SolverOutcome> CheckSat(CancellationToken cancellationToken,
       int errorLimit)
     {
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
 
-      var result = Outcome.Undetermined;
+      var result = SolverOutcome.Undetermined;
 
       if (Process == null || HadErrors)
       {
@@ -198,7 +198,7 @@ public async Task<Outcome> CheckSat(CancellationToken cancellationToken,
       }
       var errorsDiscovered = 0;
 
-      var globalResult = Outcome.Undetermined;
+      var globalResult = SolverOutcome.Undetermined;
 
       while (true)
       {
@@ -213,7 +213,7 @@ public async Task<Outcome> CheckSat(CancellationToken cancellationToken,
 
           var reporter = currentErrorHandler;
           // TODO(wuestholz): Is the reporter ever null?
-          if (usingUnsatCore && result == Outcome.Valid && reporter != null && 0 < NamedAssumes.Count)
+          if (usingUnsatCore && result == SolverOutcome.Valid && reporter != null && 0 < NamedAssumes.Count)
           {
             if (usingUnsatCore)
             {
@@ -222,16 +222,16 @@ public async Task<Outcome> CheckSat(CancellationToken cancellationToken,
             }
           }
 
-          if (libOptions.RunDiagnosticsOnTimeout && result == Outcome.TimeOut) {
+          if (libOptions.RunDiagnosticsOnTimeout && result == SolverOutcome.TimeOut) {
             (result, popLater) = await RunTimeoutDiagnostics(currentErrorHandler, result, cancellationToken);
           }
 
-          if (globalResult == Outcome.Undetermined)
+          if (globalResult == SolverOutcome.Undetermined)
           {
             globalResult = result;
           }
 
-          if (result == Outcome.Invalid)
+          if (result == SolverOutcome.Invalid)
           {
             Model model = await GetErrorModel(cancellationToken);
             if (libOptions.SIBoolControlVC)
@@ -244,7 +244,7 @@ public async Task<Outcome> CheckSat(CancellationToken cancellationToken,
               if (labels.Length == 0)
               {
                 // Without a path to an error, we don't know what to report
-                globalResult = Outcome.Undetermined;
+                globalResult = SolverOutcome.Undetermined;
                 break;
               }
             }
@@ -309,7 +309,7 @@ private T WrapInPushPop<T>(ref bool popLater, Func<T> action)
       return result;
     }
 
-    private async Task<(Outcome, bool)> RunTimeoutDiagnostics(ErrorHandler handler, Outcome result, CancellationToken cancellationToken)
+    private async Task<(SolverOutcome, bool)> RunTimeoutDiagnostics(ErrorHandler handler, SolverOutcome result, CancellationToken cancellationToken)
     {
       var popLater = false;
       if (libOptions.TraceDiagnosticsOnTimeout) {
@@ -332,9 +332,9 @@ private T WrapInPushPop<T>(ref bool popLater, Func<T> action)
           if (0 < timedOut.Count) {
             
             result = await WrapInPushPop(ref popLater, () => CheckSplit(timedOut, options.TimeLimit, timeLimitPerAssertion, ref queries, cancellationToken));
-            if (result == Outcome.Valid) {
+            if (result == SolverOutcome.Valid) {
               timedOut.Clear();
-            } else if (result == Outcome.TimeOut) {
+            } else if (result == SolverOutcome.TimeOut) {
               // Give up and report which assertions were not verified.
               var cmds = timedOut.Select(id => ctx.TimeoutDiagnosticIDToAssertion[id]);
 
@@ -343,7 +343,7 @@ private T WrapInPushPop<T>(ref bool popLater, Func<T> action)
               }
             }
           } else {
-            result = Outcome.Valid;
+            result = SolverOutcome.Valid;
           }
 
           break;
@@ -357,13 +357,13 @@ private T WrapInPushPop<T>(ref bool popLater, Func<T> action)
         
         var splitRes = await WrapInPushPop(ref popLater, () => CheckSplit(split, timeLimitPerAssertion, timeLimitPerAssertion,
           ref queries, cancellationToken));
-        if (splitRes == Outcome.Valid) {
+        if (splitRes == SolverOutcome.Valid) {
           unverified.ExceptWith(split);
           frac = 1;
-        } else if (splitRes == Outcome.Invalid) {
+        } else if (splitRes == SolverOutcome.Invalid) {
           result = splitRes;
           break;
-        } else if (splitRes == Outcome.TimeOut) {
+        } else if (splitRes == SolverOutcome.TimeOut) {
           if (2 <= frac && (4 <= (rem / frac))) {
             frac *= 4;
           } else if (2 <= (rem / frac)) {
@@ -407,7 +407,7 @@ private T WrapInPushPop<T>(ref bool popLater, Func<T> action)
       return (result, popLater);
     }
 
-    private Task<Outcome> CheckSplit(SortedSet<int> split, uint timeLimit, uint timeLimitPerAssertion,
+    private Task<SolverOutcome> CheckSplit(SortedSet<int> split, uint timeLimit, uint timeLimitPerAssertion,
       ref int queries, CancellationToken cancellationToken)
     {
       var tla = (uint)(timeLimitPerAssertion * split.Count);
@@ -497,9 +497,9 @@ private async Task<Model> GetErrorModel(CancellationToken cancellationToken)
       return resp != null ? ParseErrorModel(resp) : null;
     }
 
-    private async Task<Outcome> CheckSatAndGetResponse(CancellationToken cancellationToken)
+    private async Task<SolverOutcome> CheckSatAndGetResponse(CancellationToken cancellationToken)
     {
-      var result = Outcome.Undetermined;
+      var result = SolverOutcome.Undetermined;
       var wasUnknown = false;
 
       var checkSatResponse = await SendVcRequest("(check-sat)").WaitAsync(cancellationToken);
@@ -514,7 +514,7 @@ private async Task<Outcome> CheckSatAndGetResponse(CancellationToken cancellatio
         if (getInfoResponse != null)
         {
           result = ParseReasonUnknown(getInfoResponse, result);
-          if (result == Outcome.OutOfMemory) {
+          if (result == SolverOutcome.OutOfMemory) {
             processNeedsRestart = true;
           }
         }
@@ -523,8 +523,8 @@ private async Task<Outcome> CheckSatAndGetResponse(CancellationToken cancellatio
       if (options.Solver == SolverKind.Z3) {
         resourceCount = ParseRCount(await SendVcRequest($"(get-info :{Z3.RlimitOption})"));
         // Sometimes Z3 doesn't tell us that it ran out of resources
-        if (result != Outcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) {
-          result = Outcome.OutOfResource;
+        if (result != SolverOutcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) {
+          result = SolverOutcome.OutOfResource;
         }
       }
 
@@ -681,7 +681,7 @@ public override int GetRCount()
     /// </summary>
     static int nameCounter;
 
-    public override async Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions,
+    public override async Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions,
       ErrorHandler handler, CancellationToken cancellationToken)
     {
       currentErrorHandler = handler;
@@ -706,7 +706,7 @@ public override int GetRCount()
         PrepareCommon();
         var outcome = await CheckSat(cancellationToken, libOptions.ErrorLimit);
 
-        if (outcome != Outcome.Valid)
+        if (outcome != SolverOutcome.Valid)
         {
           Pop();
           return (outcome, new List<int>());
@@ -738,7 +738,7 @@ public override int GetRCount()
       }
     }
 
-    public override async Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
+    public override async Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
       ErrorHandler handler, CancellationToken cancellationToken)
     {
       currentErrorHandler = handler;
@@ -766,7 +766,7 @@ public override int GetRCount()
 
         PrepareCommon();
         var outcome = await CheckSatAndGetResponse(cancellationToken);
-        if (outcome != Outcome.Invalid)
+        if (outcome != SolverOutcome.Invalid)
         {
           Pop();
           return (outcome, new List<int>());
@@ -785,7 +785,7 @@ public override int GetRCount()
 
           PrepareCommon();
           outcome = await CheckSat(cancellationToken, libOptions.ErrorLimit);
-          if (outcome != Outcome.Valid)
+          if (outcome != SolverOutcome.Valid)
           {
             break;
           }
@@ -805,7 +805,7 @@ public override int GetRCount()
           k++;
         }
 
-        if (outcome == Outcome.Invalid)
+        if (outcome == SolverOutcome.Invalid)
         {
           foreach (var relaxVar in relaxVars)
           {
diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs
index 990d4791e..f037a15ec 100644
--- a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs
+++ b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs
@@ -1181,9 +1181,9 @@ public override void SetAdditionalSmtOptions(IEnumerable<OptionValue> entries)
     {
       additionalSmtOptions = entries;
     }
-    protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown)
+    protected SolverOutcome ParseOutcome(SExpr resp, out bool wasUnknown)
     {
-      var result = Outcome.Undetermined;
+      var result = SolverOutcome.Undetermined;
       wasUnknown = false;
 
       if (resp is null) {
@@ -1194,13 +1194,13 @@ protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown)
       switch (resp.Name)
       {
         case "unsat":
-          result = Outcome.Valid;
+          result = SolverOutcome.Valid;
           break;
         case "sat":
-          result = Outcome.Invalid;
+          result = SolverOutcome.Invalid;
           break;
         case "unknown":
-          result = Outcome.Invalid;
+          result = SolverOutcome.Invalid;
           wasUnknown = true;
           break;
         case "objectives":
@@ -1212,7 +1212,7 @@ protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown)
                || resp.Arguments[0].Name.Contains("resource limits reached")))
           {
             currentErrorHandler.OnResourceExceeded("max resource limit");
-            result = Outcome.OutOfResource;
+            result = SolverOutcome.OutOfResource;
           }
           else
           {
@@ -1227,9 +1227,9 @@ protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown)
       return result;
     }
 
-    protected Outcome ParseReasonUnknown(SExpr resp, Outcome initialOutcome)
+    protected SolverOutcome ParseReasonUnknown(SExpr resp, SolverOutcome initialOutcome)
     {
-      Outcome result;
+      SolverOutcome result;
       if (resp is null || resp.Name == "") {
         result = initialOutcome;
       }
@@ -1244,15 +1244,15 @@ protected Outcome ParseReasonUnknown(SExpr resp, Outcome initialOutcome)
           case "(incomplete quantifiers)":
           case "(incomplete (theory arithmetic))":
           case "smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))":
-            result = Outcome.Invalid;
+            result = SolverOutcome.Invalid;
             break;
           case "memout":
             currentErrorHandler.OnResourceExceeded("memory");
-            result = Outcome.OutOfMemory;
+            result = SolverOutcome.OutOfMemory;
             break;
           case "timeout":
             currentErrorHandler.OnResourceExceeded("timeout");
-            result = Outcome.TimeOut;
+            result = SolverOutcome.TimeOut;
             break;
           case "canceled":
             // both timeout and max resource limit are reported as
@@ -1260,12 +1260,12 @@ protected Outcome ParseReasonUnknown(SExpr resp, Outcome initialOutcome)
             if (this.options.TimeLimit > 0)
             {
               currentErrorHandler.OnResourceExceeded("timeout");
-              result = Outcome.TimeOut;
+              result = SolverOutcome.TimeOut;
             }
             else
             {
               currentErrorHandler.OnResourceExceeded("max resource limit");
-              result = Outcome.OutOfResource;
+              result = SolverOutcome.OutOfResource;
             }
 
             break;
@@ -1273,20 +1273,20 @@ protected Outcome ParseReasonUnknown(SExpr resp, Outcome initialOutcome)
           case "resource limits reached":
           case "(resource limits reached)":
             currentErrorHandler.OnResourceExceeded("max resource limit");
-            result = Outcome.OutOfResource;
+            result = SolverOutcome.OutOfResource;
             break;
           case "unknown":
-            result = Outcome.Undetermined;
+            result = SolverOutcome.Undetermined;
             break;
           default:
-            result = Outcome.Undetermined;
+            result = SolverOutcome.Undetermined;
             HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp);
             break;
         }
       }
       else
       {
-        result = Outcome.Undetermined;
+        result = SolverOutcome.Undetermined;
         HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp);
       }
 
diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
index 3ac3068df..7eda7869a 100644
--- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
+++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
@@ -353,7 +353,7 @@ public async Task StatusTest() {
     Assert.Contains(assertion, perAssertCounterExamples.Keys);
     var outcomeAssertion = perAssertOutcome[assertion];
     var counterExampleAssertion = perAssertCounterExamples[assertion];
-    Assert.AreEqual(Outcome.Invalid, outcomeAssertion);
+    Assert.AreEqual(SolverOutcome.Invalid, outcomeAssertion);
     Assert.AreEqual(true, counterExampleAssertion is AssertCounterexample);
     var assertCounterexample = (AssertCounterexample)counterExampleAssertion;
     Assert.AreEqual(assertCounterexample.FailingAssert, assertion);
diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs
index 6ce4cc4cc..125552d7d 100644
--- a/Source/VCGeneration/Checker.cs
+++ b/Source/VCGeneration/Checker.cs
@@ -40,7 +40,7 @@ void ObjectInvariant()
     private ProverInterface thmProver;
 
     // state for the async interface
-    private volatile Outcome outcome;
+    private volatile SolverOutcome outcome;
     private volatile bool hasOutput;
     private volatile UnexpectedProverOutputException outputExn;
     public DateTime ProverStart { get; private set; }
@@ -292,22 +292,22 @@ private async Task Check(string descriptiveName, VCExpr vc, CancellationToken ca
 
       switch (outcome)
       {
-        case Outcome.Valid:
+        case SolverOutcome.Valid:
           thmProver.LogComment("Valid");
           break;
-        case Outcome.Invalid:
+        case SolverOutcome.Invalid:
           thmProver.LogComment("Invalid");
           break;
-        case Outcome.TimeOut:
+        case SolverOutcome.TimeOut:
           thmProver.LogComment("Timed out");
           break;
-        case Outcome.OutOfResource:
+        case SolverOutcome.OutOfResource:
           thmProver.LogComment("Out of resource");
           break;
-        case Outcome.OutOfMemory:
+        case SolverOutcome.OutOfMemory:
           thmProver.LogComment("Out of memory");
           break;
-        case Outcome.Undetermined:
+        case SolverOutcome.Undetermined:
           thmProver.LogComment("Undetermined");
           break;
       }
@@ -341,7 +341,7 @@ public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.
       ProverTask = Check(descriptiveName, vc, cancellationToken);
     }
 
-    public Outcome ReadOutcome()
+    public SolverOutcome ReadOutcome()
     {
       Contract.Requires(IsBusy);
       Contract.Requires(HasOutput);
@@ -389,7 +389,7 @@ public override Task GoBackToIdle()
       throw new NotImplementedException();
     }
 
-    public override Task<Outcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit,
+    public override Task<SolverOutcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit,
       CancellationToken cancellationToken) {
       throw new NotImplementedException();
     }
diff --git a/Source/VCGeneration/CommandTransformations.cs b/Source/VCGeneration/CommandTransformations.cs
index a39bac235..74daf7195 100644
--- a/Source/VCGeneration/CommandTransformations.cs
+++ b/Source/VCGeneration/CommandTransformations.cs
@@ -9,7 +9,7 @@ public static Cmd AssertIntoAssume(VCGenOptions options, Cmd c)
   {
     if (c is AssertCmd assrt)
     {
-      return VCGen.AssertTurnedIntoAssume(options, assrt);
+      return VerificationConditionGenerator.AssertTurnedIntoAssume(options, assrt);
     }
 
     return c;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 418d47198..4a8b93924 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -44,21 +44,21 @@ public ConditionGenerationContracts(Program program, CheckerPool checkerPool)
   [ContractClass(typeof(ConditionGenerationContracts))]
   public abstract class ConditionGeneration : IDisposable
   {
-    public static VcOutcome ProverInterfaceOutcomeToConditionGenerationOutcome(Microsoft.Boogie.Outcome outcome)
+    public static VcOutcome ProverInterfaceOutcomeToConditionGenerationOutcome(Microsoft.Boogie.SolverOutcome outcome)
     {
       switch (outcome)
       {
-        case Microsoft.Boogie.Outcome.Invalid:
+        case Microsoft.Boogie.SolverOutcome.Invalid:
           return VcOutcome.Errors;
-        case Microsoft.Boogie.Outcome.OutOfMemory:
+        case Microsoft.Boogie.SolverOutcome.OutOfMemory:
           return VcOutcome.OutOfMemory;
-        case Microsoft.Boogie.Outcome.TimeOut:
+        case Microsoft.Boogie.SolverOutcome.TimeOut:
           return VcOutcome.TimedOut;
-        case Microsoft.Boogie.Outcome.OutOfResource:
+        case Microsoft.Boogie.SolverOutcome.OutOfResource:
           return VcOutcome.OutOfResource;
-        case Microsoft.Boogie.Outcome.Undetermined:
+        case Microsoft.Boogie.SolverOutcome.Undetermined:
           return VcOutcome.Inconclusive;
-        case Microsoft.Boogie.Outcome.Valid:
+        case Microsoft.Boogie.SolverOutcome.Valid:
           return VcOutcome.Correct;
       }
 
diff --git a/Source/VCGeneration/Counterexample.cs b/Source/VCGeneration/Counterexample.cs
index 457568fdd..11e5ff3d9 100644
--- a/Source/VCGeneration/Counterexample.cs
+++ b/Source/VCGeneration/Counterexample.cs
@@ -196,7 +196,7 @@ public void Print(int indent, TextWriter tw, Action<Block> blockAction = null)
               {
                 var cmd = GetTraceCmd(loc);
                 var calleeName = GetCalledProcName(cmd);
-                if (calleeName.StartsWith(VC.StratifiedVCGenBase.recordProcName) &&
+                if (calleeName.StartsWith(VC.StratifiedVerificationConditionGeneratorBase.recordProcName) &&
                     options.StratifiedInlining > 0)
                 {
                   Contract.Assert(calleeCounterexamples[loc].args.Count == 1);
diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs
index e08874579..72c3c76c8 100644
--- a/Source/VCGeneration/FocusAttribute.cs
+++ b/Source/VCGeneration/FocusAttribute.cs
@@ -15,7 +15,7 @@ namespace VCGeneration;
 
 public static class FocusAttribute
 {
-  public static List<Split> FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VCGen par)
+  public static List<Split> FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerificationConditionGenerator par)
   {
     bool IsFocusCmd(Cmd c) {
       return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus");
diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs
index 76c3922d6..5646d71fa 100644
--- a/Source/VCGeneration/ManualSplitFinder.cs
+++ b/Source/VCGeneration/ManualSplitFinder.cs
@@ -9,7 +9,7 @@ namespace VCGeneration;
 public static class ManualSplitFinder
 {
   
-  public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VCGen par, bool splitOnEveryAssert)
+  public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerificationConditionGenerator par, bool splitOnEveryAssert)
   {
     List<Split> focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par);
     var splits = focussedImpl.Select(s => FindManualSplits(s, splitOnEveryAssert)).SelectMany(x => x).ToList();
diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs
index 432236303..a56cd5ff6 100644
--- a/Source/VCGeneration/SmokeTester.cs
+++ b/Source/VCGeneration/SmokeTester.cs
@@ -24,7 +24,7 @@ void ObjectInvariant()
     Contract.Invariant(callback != null);
   }
 
-  VCGen parent;
+  VerificationConditionGenerator parent;
   ImplementationRun run;
   Block initial;
   int id;
@@ -32,7 +32,7 @@ void ObjectInvariant()
   HashSet<Block> visited = new HashSet<Block>();
   VerifierCallback callback;
 
-  internal SmokeTester(VCGen par, ImplementationRun run, VerifierCallback callback)
+  internal SmokeTester(VerificationConditionGenerator par, ImplementationRun run, VerifierCallback callback)
   {
     Contract.Requires(par != null);
     Contract.Requires(run != null);
@@ -130,7 +130,7 @@ Block CopyBlock(Block b)
       }
       else
       {
-        seq.Add(VCGen.AssertTurnedIntoAssume(Options, turn));
+        seq.Add(VerificationConditionGenerator.AssertTurnedIntoAssume(Options, turn));
       }
     }
 
@@ -278,7 +278,7 @@ async Task<bool> CheckUnreachable(TextWriter traceWriter, Block cur, List<Cmd> s
     Checker checker = await parent.CheckerPool.FindCheckerFor(parent, null, CancellationToken.None);
     Contract.Assert(checker != null);
 
-    Outcome outcome = Outcome.Undetermined;
+    SolverOutcome outcome = SolverOutcome.Undetermined;
     try
     {
       VCExpr vc;
@@ -327,12 +327,12 @@ async Task<bool> CheckUnreachable(TextWriter traceWriter, Block cur, List<Cmd> s
     if (Options.Trace)
     {
       traceWriter.WriteLine("  [{0} s] {1}", elapsed.TotalSeconds,
-        outcome == Outcome.Valid
+        outcome == SolverOutcome.Valid
           ? "OOPS"
-          : "OK" + (outcome == Outcome.Invalid ? "" : " (" + outcome + ")"));
+          : "OK" + (outcome == SolverOutcome.Invalid ? "" : " (" + outcome + ")"));
     }
 
-    if (outcome == Outcome.Valid)
+    if (outcome == SolverOutcome.Valid)
     {
       // copy it again, so we get the version with calls, assignments and such
       copy = CopyBlock(cur);
diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs
index e6fb880d7..fdcf1e80f 100644
--- a/Source/VCGeneration/Split.cs
+++ b/Source/VCGeneration/Split.cs
@@ -64,7 +64,7 @@ void ObjectInvariant()
 
       public Dictionary<TransferCmd, ReturnCmd> GotoCmdOrigins { get; }
 
-      public readonly VCGen /*!*/ parent;
+      public readonly VerificationConditionGenerator /*!*/ parent;
 
       public Implementation /*!*/ Implementation => Run.Implementation;
 
@@ -84,11 +84,11 @@ void ObjectInvariant()
 
       // async interface
       public int SplitIndex { get; set; }
-      internal VCGen.ErrorReporter reporter;
+      internal VerificationConditionGenerator.ErrorReporter reporter;
 
       public Split(VCGenOptions options, List<Block /*!*/> /*!*/ blocks,
         Dictionary<TransferCmd, ReturnCmd> /*!*/ gotoCmdOrigins,
-        VCGen /*!*/ par, ImplementationRun run)
+        VerificationConditionGenerator /*!*/ par, ImplementationRun run)
       {
         Contract.Requires(cce.NonNullElements(blocks));
         Contract.Requires(gotoCmdOrigins != null);
@@ -616,7 +616,7 @@ List<Cmd> SliceCmds(Block b)
 
             if (swap)
             {
-              theNewCmd = VCGen.AssertTurnedIntoAssume(Options, a);
+              theNewCmd = VerificationConditionGenerator.AssertTurnedIntoAssume(Options, a);
             }
           }
 
@@ -756,7 +756,7 @@ public Counterexample ToCounterexample(ProverContext context)
             Contract.Assert(c != null);
             if (c is AssertCmd)
             {
-              var counterexample = VCGen.AssertCmdToCounterexample(Options, (AssertCmd) c, cce.NonNull(b.TransferCmd), trace, null, null, null, context, this);
+              var counterexample = VerificationConditionGenerator.AssertCmdToCounterexample(Options, (AssertCmd) c, cce.NonNull(b.TransferCmd), trace, null, null, null, context, this);
               Counterexamples.Add(counterexample);
               return counterexample;
             }
@@ -883,10 +883,10 @@ public Counterexample ToCounterexample(ProverContext context)
         return result;
       }
 
-      public (Bpl.Outcome outcome, VerificationRunResult result, int resourceCount) ReadOutcome(int iteration, Checker checker, VerifierCallback callback)
+      public (Bpl.SolverOutcome outcome, VerificationRunResult result, int resourceCount) ReadOutcome(int iteration, Checker checker, VerifierCallback callback)
       {
         Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-        Bpl.Outcome outcome = cce.NonNull(checker).ReadOutcome();
+        Bpl.SolverOutcome outcome = cce.NonNull(checker).ReadOutcome();
 
         if (Options.Trace && SplitIndex >= 0)
         {
@@ -943,7 +943,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa
 
           ProverContext ctx = checker.TheoremProver.Context;
           Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;
-          var cc = new VCGen.CodeExprConversionClosure(traceWriter, checker.Pool.Options, absyIds, ctx);
+          var cc = new VerificationConditionGenerator.CodeExprConversionClosure(traceWriter, checker.Pool.Options, absyIds, ctx);
           bet.SetCodeExprConverter(cc.CodeExprToVerificationCondition);
 
           var exprGen = ctx.ExprGen;
@@ -957,7 +957,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa
             exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
           VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(absyIds.GetId(Implementation.Blocks[0]))));
           vc = exprGen.Implies(eqExpr, vc);
-          reporter = new VCGen.ErrorReporter(Options, GotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback,
+          reporter = new VerificationConditionGenerator.ErrorReporter(Options, GotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback,
             mvInfo, checker.TheoremProver.Context, parent.program, this);
         }
 
diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs
index d361ada9a..7409ca17e 100644
--- a/Source/VCGeneration/SplitAndVerifyWorker.cs
+++ b/Source/VCGeneration/SplitAndVerifyWorker.cs
@@ -9,7 +9,6 @@
 using Microsoft.Boogie;
 using VCGeneration;
 using static VC.ConditionGeneration;
-using Outcome = Microsoft.Boogie.Outcome;
 
 namespace VC
 {
@@ -32,7 +31,7 @@ class SplitAndVerifyWorker
     private bool TrackingProgress => DoSplitting && (callback.OnProgress != null || options.Trace); 
     private bool KeepGoing => maxKeepGoingSplits > 1;
 
-    private VCGen vcGen;
+    private VerificationConditionGenerator verificationConditionGenerator;
     private VcOutcome vcOutcome;
     private double remainingCost;
     private double provenCost;
@@ -41,7 +40,7 @@ class SplitAndVerifyWorker
 
     private int totalResourceCount;
 
-    public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun run,
+    public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, ImplementationRun run,
       Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo,
       VcOutcome vcOutcome)
     {
@@ -50,16 +49,16 @@ public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun
       this.mvInfo = mvInfo;
       this.run = run;
       this.vcOutcome = vcOutcome;
-      this.vcGen = vcGen;
+      this.verificationConditionGenerator = verificationConditionGenerator;
       var maxSplits = options.VcsMaxSplits;
-      VCGen.CheckIntAttributeOnImpl(run, "vcs_max_splits", ref maxSplits);
+      VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_splits", ref maxSplits);
       
       maxKeepGoingSplits = options.VcsMaxKeepGoingSplits;
-      VCGen.CheckIntAttributeOnImpl(run, "vcs_max_keep_going_splits", ref maxKeepGoingSplits);
+      VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_keep_going_splits", ref maxKeepGoingSplits);
       
       maxVcCost = options.VcsMaxCost;
       var tmpMaxVcCost = -1;
-      VCGen.CheckIntAttributeOnImpl(run, "vcs_max_cost", ref tmpMaxVcCost);
+      VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_cost", ref tmpMaxVcCost);
       if (tmpMaxVcCost >= 0)
       {
         maxVcCost = tmpMaxVcCost;
@@ -69,7 +68,7 @@ public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun
       Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert);
 
       ResetPredecessors(Implementation.Blocks);
-      manualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, vcGen, splitOnEveryAssert);
+      manualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator, splitOnEveryAssert);
       
       if (manualSplits.Count == 1 && maxSplits > 1) {
         manualSplits = Split.DoSplit(manualSplits[0], maxVcCost, maxSplits);
@@ -197,17 +196,17 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch
       }
     }
 
-    private static bool IsProverFailed(Outcome outcome)
+    private static bool IsProverFailed(SolverOutcome outcome)
     {
       switch (outcome)
       {
-        case Outcome.Valid:
-        case Outcome.Invalid:
-        case Outcome.Undetermined:
+        case SolverOutcome.Valid:
+        case SolverOutcome.Invalid:
+        case SolverOutcome.Undetermined:
           return false;
-        case Outcome.OutOfMemory:
-        case Outcome.TimeOut:
-        case Outcome.OutOfResource:
+        case SolverOutcome.OutOfMemory:
+        case SolverOutcome.TimeOut:
+        case SolverOutcome.OutOfResource:
           return true;
         default:
           Contract.Assert(false);
@@ -215,36 +214,36 @@ private static bool IsProverFailed(Outcome outcome)
       }
     }
 
-    private static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, Outcome newOutcome)
+    private static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, SolverOutcome newOutcome)
     {
       switch (newOutcome)
       {
-        case Outcome.Valid:
+        case SolverOutcome.Valid:
           return currentVcOutcome;
-        case Outcome.Invalid:
+        case SolverOutcome.Invalid:
           return VcOutcome.Errors;
-        case Outcome.OutOfMemory:
+        case SolverOutcome.OutOfMemory:
           if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive)
           {
             return VcOutcome.OutOfMemory;
           }
 
           return currentVcOutcome;
-        case Outcome.TimeOut:
+        case SolverOutcome.TimeOut:
           if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive)
           {
             return VcOutcome.TimedOut;
           }
 
           return currentVcOutcome;
-        case Outcome.OutOfResource:
+        case SolverOutcome.OutOfResource:
           if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive)
           {
             return VcOutcome.OutOfResource;
           }
 
           return currentVcOutcome;
-        case Outcome.Undetermined:
+        case SolverOutcome.Undetermined:
           if (currentVcOutcome != VcOutcome.Errors)
           {
             return VcOutcome.Inconclusive;
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index beb082cb5..5a296ffc4 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -348,7 +348,7 @@ public override string ToString()
   public class StratifiedInliningInfo
   {
     private VCGenOptions options;
-    public StratifiedVCGenBase vcgen;
+    public StratifiedVerificationConditionGeneratorBase vcgen;
     public ImplementationRun run;
     public Function function;
     public Variable controlFlowVariable;
@@ -370,10 +370,10 @@ public class StratifiedInliningInfo
 
     public Implementation Implementation => run.Implementation;
 
-    public StratifiedInliningInfo(VCGenOptions options, ImplementationRun run, StratifiedVCGenBase stratifiedVcGen,
+    public StratifiedInliningInfo(VCGenOptions options, ImplementationRun run, StratifiedVerificationConditionGeneratorBase stratifiedVerificationConditionGenerator,
       Action<Implementation> PassiveImplInstrumentation)
     {
-      vcgen = stratifiedVcGen;
+      vcgen = stratifiedVerificationConditionGenerator;
       this.PassiveImplInstrumentation = PassiveImplInstrumentation;
       this.run = run;
       this.options = options;
@@ -655,7 +655,7 @@ public void GenerateVC()
 
       var absyIds = new ControlFlowIdMap<Absy>();
       
-      VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(run.OutputWriter, options, absyIds, proverInterface.Context);
+      VerificationConditionGenerator.CodeExprConversionClosure cc = new VerificationConditionGenerator.CodeExprConversionClosure(run.OutputWriter, options, absyIds, proverInterface.Context);
       translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition);
       vcexpr = gen.Not(vcgen.GenerateVCAux(Implementation, controlFlowVariableExpr, absyIds, proverInterface.Context));
 
@@ -702,14 +702,14 @@ public void GenerateVC()
   }
 
   // This class is derived and used by Corral to create VCs for Stratified Inlining.
-  public abstract class StratifiedVCGenBase : VCGen
+  public abstract class StratifiedVerificationConditionGeneratorBase : VerificationConditionGenerator
   {
     public readonly static string recordProcName = "boogie_si_record";
     public readonly static string callSiteVarAttr = "callSiteVar";
     public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
     public ProverInterface prover;
 
-    public StratifiedVCGenBase(TextWriter traceWriter, VCGenOptions options, Program program, string logFilePath /*?*/, bool appendLogFile, CheckerPool checkerPool,
+    public StratifiedVerificationConditionGeneratorBase(TextWriter traceWriter, VCGenOptions options, Program program, string logFilePath /*?*/, bool appendLogFile, CheckerPool checkerPool,
       Action<Implementation> PassiveImplInstrumentation)
       : base(program, checkerPool)
     {
diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VerificationConditionGenerator.cs
similarity index 99%
rename from Source/VCGeneration/VCGen.cs
rename to Source/VCGeneration/VerificationConditionGenerator.cs
index c0abd717d..a74738744 100644
--- a/Source/VCGeneration/VCGen.cs
+++ b/Source/VCGeneration/VerificationConditionGenerator.cs
@@ -18,14 +18,14 @@ namespace VC
   using Bpl = Microsoft.Boogie;
   using System.Threading.Tasks;
 
-  public class VCGen : ConditionGeneration
+  public class VerificationConditionGenerator : ConditionGeneration
   {
     
     /// <summary>
     /// Constructor.  Initializes the theorem prover.
     /// </summary>
     [NotDelayed]
-    public VCGen(Program program, CheckerPool checkerPool)
+    public VerificationConditionGenerator(Program program, CheckerPool checkerPool)
       : base(program, checkerPool)
     {
       Contract.Requires(program != null);
@@ -89,7 +89,7 @@ public CodeExprConversionClosure(TextWriter traceWriter, VCGenOptions options, C
 
       public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List<VCExprLetBinding> bindings, bool isPositiveContext, Dictionary<Cmd, List<object>> debugInfos)
       {
-        VCGen vcgen = new VCGen(new Program(), new CheckerPool(options));
+        VerificationConditionGenerator vcgen = new VerificationConditionGenerator(new Program(), new CheckerPool(options));
         vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();
         vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();
         vcgen.CurrentLocalVariables = codeExpr.LocVars;
@@ -501,7 +501,7 @@ public ErrorReporter(VCGenOptions options,
       }
 
       public override void OnModel(IList<string> labels /*!*/ /*!*/, Model model,
-        Bpl.Outcome proverOutcome)
+        Bpl.SolverOutcome proverOutcome)
       {
         // no counter examples reported.
         if (labels.Count == 0)
diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs
index c26e859a5..5704dca80 100644
--- a/Source/VCGeneration/VerificationRunResult.cs
+++ b/Source/VCGeneration/VerificationRunResult.cs
@@ -20,7 +20,7 @@ public record VerificationRunResult
     int VcNum,
     int Iteration,
     DateTime StartTime,
-    Bpl.Outcome Outcome,
+    Bpl.SolverOutcome Outcome,
     TimeSpan RunTime,
     int MaxCounterExamples,
     List<Counterexample> CounterExamples,
@@ -29,12 +29,12 @@ public record VerificationRunResult
     int ResourceCount,
     SolverKind? SolverUsed
   ) {
-    public void ComputePerAssertOutcomes(out Dictionary<AssertCmd, Bpl.Outcome> perAssertOutcome,
+    public void ComputePerAssertOutcomes(out Dictionary<AssertCmd, Bpl.SolverOutcome> perAssertOutcome,
       out Dictionary<AssertCmd, Counterexample> perAssertCounterExamples) {
       perAssertOutcome = new();
       perAssertCounterExamples = new();
-      if (Outcome == Bpl.Outcome.Valid) {
-        perAssertOutcome = Asserts.ToDictionary(cmd => cmd, assertCmd => Bpl.Outcome.Valid);
+      if (Outcome == Bpl.SolverOutcome.Valid) {
+        perAssertOutcome = Asserts.ToDictionary(cmd => cmd, assertCmd => Bpl.SolverOutcome.Valid);
       } else {
         foreach (var counterExample in CounterExamples) {
           AssertCmd underlyingAssert;
@@ -53,17 +53,17 @@ public void ComputePerAssertOutcomes(out Dictionary<AssertCmd, Bpl.Outcome> perA
             continue;
           }
 
-          perAssertOutcome.TryAdd(underlyingAssert, Bpl.Outcome.Invalid);
+          perAssertOutcome.TryAdd(underlyingAssert, Bpl.SolverOutcome.Invalid);
           perAssertCounterExamples.TryAdd(underlyingAssert, counterExample);
         }
 
         var remainingOutcome =
-          Outcome == Bpl.Outcome.Invalid && CounterExamples.Count < MaxCounterExamples
+          Outcome == Bpl.SolverOutcome.Invalid && CounterExamples.Count < MaxCounterExamples
             // We could not extract more counterexamples, remaining assertions are thus valid 
-            ? Bpl.Outcome.Valid
-            : Outcome == Bpl.Outcome.Invalid
+            ? Bpl.SolverOutcome.Valid
+            : Outcome == Bpl.SolverOutcome.Invalid
               // We reached the maximum number of counterexamples, we can't infer anything for the remaining assertions
-              ? Bpl.Outcome.Undetermined
+              ? Bpl.SolverOutcome.Undetermined
               // TimeOut, OutOfMemory, OutOfResource, Undetermined for a single split also applies to assertions
               : Outcome;