diff --git a/Source/ExecutionEngine/ConsolePrinter.cs b/Source/ExecutionEngine/ConsolePrinter.cs
index b47bfae5f..16649a7ab 100644
--- a/Source/ExecutionEngine/ConsolePrinter.cs
+++ b/Source/ExecutionEngine/ConsolePrinter.cs
@@ -206,11 +206,11 @@ public virtual void ReportStartVerifyImplementation(Implementation implementatio
     // Do not print anything to console
   }
 
-  public virtual void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result) {
+  public virtual void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result) {
     // Do not print anything to console
   }
 
-  public virtual void ReportSplitResult(Split split, VCResult splitResult) {
+  public virtual void ReportSplitResult(Split split, VerificationRunResult splitResult) {
     // Do not print anything to console
   }
 }
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index ed96e80f4..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, VerificationResult> PostProcessResult) {
+  public record ProcessedProgram(Program Program, Action<VerificationConditionGenerator, Implementation, ImplementationRunResult> PostProcessResult) {
     public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) {
     }
   }
@@ -828,10 +828,10 @@ private IObservable<IVerificationStatus> VerifyImplementation(
       string programId,
       TextWriter traceWriter)
     {
-      VerificationResult verificationResult = GetCachedVerificationResult(implementation, traceWriter);
-      if (verificationResult != null) {
-        UpdateCachedStatistics(stats, verificationResult.Outcome, verificationResult.Errors);
-        return Observable.Return(new Completed(verificationResult));
+      ImplementationRunResult implementationRunResult = GetCachedVerificationResult(implementation, traceWriter);
+      if (implementationRunResult != null) {
+        UpdateCachedStatistics(stats, implementationRunResult.VcOutcome, implementationRunResult.Errors);
+        return Observable.Return(new Completed(implementationRunResult));
       }
       Options.Printer.Inform("", traceWriter); // newline
       Options.Printer.Inform($"Verifying {implementation.VerboseName} ...", traceWriter);
@@ -849,7 +849,7 @@ private IObservable<IVerificationStatus> VerifyImplementation(
       return Observable.Return(new Running()).Concat(afterRunningStates);
     }
 
-    public VerificationResult GetCachedVerificationResult(Implementation impl, TextWriter output)
+    public ImplementationRunResult GetCachedVerificationResult(Implementation impl, TextWriter output)
     {
       if (0 >= Options.VerifySnapshots)
       {
@@ -863,7 +863,7 @@ public VerificationResult GetCachedVerificationResult(Implementation impl, TextW
       }
 
       if (Options.VerifySnapshots < 3 ||
-          cachedResults.Outcome == ConditionGeneration.Outcome.Correct) {
+          cachedResults.VcOutcome == VcOutcome.Correct) {
         Options.Printer.Inform($"Retrieving cached verification result for implementation {impl.VerboseName}...", output);
         return cachedResults;
       }
@@ -875,19 +875,19 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc
       PipelineStatistics stats, ErrorReporterDelegate er, CancellationToken cancellationToken,
       string programId, Implementation impl, TextWriter traceWriter)
     {
-      var verificationResult = new VerificationResult(impl, programId);
+      var verificationResult = new ImplementationRunResult(impl, programId);
 
-      var batchCompleted = new Subject<(Split split, VCResult vcResult)>();
+      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;
 
         try
         {
-          (verificationResult.Outcome, verificationResult.Errors, verificationResult.VCResults) =
+          (verificationResult.VcOutcome, verificationResult.Errors, verificationResult.VCResults) =
             await vcgen.VerifyImplementation(new ImplementationRun(impl, traceWriter), batchCompleted, cancellationToken);
           processedProgram.PostProcessResult(vcgen, impl, verificationResult);
         }
@@ -906,7 +906,7 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc
           }
 
           verificationResult.Errors = null;
-          verificationResult.Outcome = ConditionGeneration.Outcome.Inconclusive;
+          verificationResult.VcOutcome = VcOutcome.Inconclusive;
         }
         catch (ProverDiedException)
         {
@@ -918,14 +918,14 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc
             "Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}",
             impl.VerboseName, upo.Message);
           verificationResult.Errors = null;
-          verificationResult.Outcome = ConditionGeneration.Outcome.Inconclusive;
+          verificationResult.VcOutcome = VcOutcome.Inconclusive;
         }
         catch (IOException e)
         {
           Options.Printer.AdvisoryWriteLine(traceWriter, "Advisory: {0} SKIPPED due to I/O exception: {1}",
             impl.VerboseName, e.Message);
           verificationResult.Errors = null;
-          verificationResult.Outcome = ConditionGeneration.Outcome.SolverException;
+          verificationResult.VcOutcome = VcOutcome.SolverException;
         }
 
         verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount;
@@ -993,8 +993,8 @@ private async Task<PipelineOutcome> RunHoudini(Program program, PipelineStatisti
 
       foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
       {
-        ProcessOutcome(Options.Printer, x.outcome, x.errors, "", stats, outputWriter, Options.TimeLimit, er);
-        ProcessErrors(Options.Printer, x.errors, x.outcome, outputWriter, er);
+        ProcessOutcome(Options.Printer, x.VcOutcome, x.errors, "", stats, outputWriter, Options.TimeLimit, er);
+        ProcessErrors(Options.Printer, x.errors, x.VcOutcome, outputWriter, er);
       }
 
       return PipelineOutcome.Done;
@@ -1046,8 +1046,8 @@ private async Task<PipelineOutcome> RunStagedHoudini(Program program, PipelineSt
 
       foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
       {
-        ProcessOutcome(Options.Printer, x.outcome, x.errors, "", stats, Options.OutputWriter, Options.TimeLimit, er);
-        ProcessErrors(Options.Printer, x.errors, x.outcome, Options.OutputWriter, er);
+        ProcessOutcome(Options.Printer, x.VcOutcome, x.errors, "", stats, Options.OutputWriter, Options.TimeLimit, er);
+        ProcessErrors(Options.Printer, x.errors, x.VcOutcome, Options.OutputWriter, er);
       }
 
       return PipelineOutcome.Done;
@@ -1055,24 +1055,24 @@ private async Task<PipelineOutcome> RunStagedHoudini(Program program, PipelineSt
 
     #endregion
 
-    public void ProcessOutcome(OutputPrinter printer, ConditionGeneration.Outcome outcome, List<Counterexample> errors, string timeIndication,
+    public void ProcessOutcome(OutputPrinter printer, VcOutcome vcOutcome, List<Counterexample> errors, string timeIndication,
       PipelineStatistics stats, TextWriter tw, uint timeLimit, ErrorReporterDelegate er = null, string implName = null,
       IToken implTok = null, string msgIfVerifies = null)
     {
       Contract.Requires(stats != null);
 
-      UpdateStatistics(stats, outcome, errors);
+      UpdateStatistics(stats, vcOutcome, errors);
 
-      printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
+      printer.Inform(timeIndication + OutcomeIndication(vcOutcome, errors), tw);
 
-      ReportOutcome(printer, outcome, er, implName, implTok, msgIfVerifies, tw, timeLimit, errors);
+      ReportOutcome(printer, vcOutcome, er, implName, implTok, msgIfVerifies, tw, timeLimit, errors);
     }
 
     public void ReportOutcome(OutputPrinter printer,
-      ConditionGeneration.Outcome outcome, ErrorReporterDelegate er, string implName,
+      VcOutcome vcOutcome, ErrorReporterDelegate er, string implName,
       IToken implTok, string msgIfVerifies, TextWriter tw, uint timeLimit, List<Counterexample> errors) {
 
-      var errorInfo = GetOutcomeError(Options, outcome, implName, implTok, msgIfVerifies, tw, timeLimit, errors);
+      var errorInfo = GetOutcomeError(Options, vcOutcome, implName, implTok, msgIfVerifies, tw, timeLimit, errors);
       if (errorInfo != null)
       {
         errorInfo.ImplementationName = implName;
@@ -1088,25 +1088,25 @@ public void ReportOutcome(OutputPrinter printer,
       }
     }
 
-    internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options, ConditionGeneration.Outcome outcome, string implName, IToken implTok, string msgIfVerifies,
+    internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options, VcOutcome vcOutcome, string implName, IToken implTok, string msgIfVerifies,
       TextWriter tw, uint timeLimit, List<Counterexample> errors)
     {
       ErrorInformation errorInfo = null;
 
-      switch (outcome) {
-        case VCGen.Outcome.Correct:
+      switch (vcOutcome) {
+        case VcOutcome.Correct:
           if (msgIfVerifies != null) {
             tw.WriteLine(msgIfVerifies);
           }
 
           break;
-        case VCGen.Outcome.ReachedBound:
+        case VcOutcome.ReachedBound:
           tw.WriteLine($"Stratified Inlining: Reached recursion bound of {options.RecursionBound}");
           break;
-        case VCGen.Outcome.Errors:
-        case VCGen.Outcome.TimedOut:
+        case VcOutcome.Errors:
+        case VcOutcome.TimedOut:
           if (implName != null && implTok != null) {
-            if (outcome == ConditionGeneration.Outcome.TimedOut ||
+            if (vcOutcome == VcOutcome.TimedOut ||
                 (errors != null && errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts))) {
               string msg = string.Format("Verification of '{1}' timed out after {0} seconds", timeLimit, implName);
               errorInfo = ErrorInformation.Create(implTok, msg);
@@ -1148,21 +1148,21 @@ internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options,
           }
 
           break;
-        case VCGen.Outcome.OutOfResource:
+        case VcOutcome.OutOfResource:
           if (implName != null && implTok != null) {
             string msg = "Verification out of resource (" + implName + ")";
             errorInfo = ErrorInformation.Create(implTok, msg);
           }
 
           break;
-        case VCGen.Outcome.OutOfMemory:
+        case VcOutcome.OutOfMemory:
           if (implName != null && implTok != null) {
             string msg = "Verification out of memory (" + implName + ")";
             errorInfo = ErrorInformation.Create(implTok, msg);
           }
 
           break;
-        case VCGen.Outcome.SolverException:
+        case VcOutcome.SolverException:
           if (implName != null && implTok != null) {
             string msg = "Verification encountered solver exception (" + implName + ")";
             errorInfo = ErrorInformation.Create(implTok, msg);
@@ -1170,7 +1170,7 @@ internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options,
 
           break;
 
-        case VCGen.Outcome.Inconclusive:
+        case VcOutcome.Inconclusive:
           if (implName != null && implTok != null) {
             string msg = "Verification inconclusive (" + implName + ")";
             errorInfo = ErrorInformation.Create(implTok, msg);
@@ -1183,36 +1183,36 @@ internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options,
     }
 
 
-    private static string OutcomeIndication(VC.VCGen.Outcome outcome, List<Counterexample> errors)
+    private static string OutcomeIndication(VcOutcome vcOutcome, List<Counterexample> errors)
     {
       string traceOutput = "";
-      switch (outcome)
+      switch (vcOutcome)
       {
         default:
           Contract.Assert(false); // unexpected outcome
           throw new cce.UnreachableException();
-        case VCGen.Outcome.ReachedBound:
+        case VcOutcome.ReachedBound:
           traceOutput = "verified";
           break;
-        case VCGen.Outcome.Correct:
+        case VcOutcome.Correct:
           traceOutput = "verified";
           break;
-        case VCGen.Outcome.TimedOut:
+        case VcOutcome.TimedOut:
           traceOutput = "timed out";
           break;
-        case VCGen.Outcome.OutOfResource:
+        case VcOutcome.OutOfResource:
           traceOutput = "out of resource";
           break;
-        case VCGen.Outcome.OutOfMemory:
+        case VcOutcome.OutOfMemory:
           traceOutput = "out of memory";
           break;
-        case VCGen.Outcome.SolverException:
+        case VcOutcome.SolverException:
           traceOutput = "solver exception";
           break;
-        case VCGen.Outcome.Inconclusive:
+        case VcOutcome.Inconclusive:
           traceOutput = "inconclusive";
           break;
-        case VCGen.Outcome.Errors:
+        case VcOutcome.Errors:
           Contract.Assert(errors != null);
           traceOutput = string.Format("error{0}", errors.Count == 1 ? "" : "s");
           break;
@@ -1222,44 +1222,44 @@ private static string OutcomeIndication(VC.VCGen.Outcome outcome, List<Counterex
     }
 
 
-    private static void UpdateStatistics(PipelineStatistics stats, VC.VCGen.Outcome outcome, List<Counterexample> errors)
+    private static void UpdateStatistics(PipelineStatistics stats, VcOutcome vcOutcome, List<Counterexample> errors)
     {
       Contract.Requires(stats != null);
 
-      switch (outcome)
+      switch (vcOutcome)
       {
         default:
           Contract.Assert(false); // unexpected outcome
           throw new cce.UnreachableException();
-        case VCGen.Outcome.ReachedBound:
+        case VcOutcome.ReachedBound:
           Interlocked.Increment(ref stats.VerifiedCount);
 
           break;
-        case VCGen.Outcome.Correct:
+        case VcOutcome.Correct:
           Interlocked.Increment(ref stats.VerifiedCount);
 
           break;
-        case VCGen.Outcome.TimedOut:
+        case VcOutcome.TimedOut:
           Interlocked.Increment(ref stats.TimeoutCount);
 
           break;
-        case VCGen.Outcome.OutOfResource:
+        case VcOutcome.OutOfResource:
           Interlocked.Increment(ref stats.OutOfResourceCount);
 
           break;
-        case VCGen.Outcome.OutOfMemory:
+        case VcOutcome.OutOfMemory:
           Interlocked.Increment(ref stats.OutOfMemoryCount);
 
           break;
-        case VCGen.Outcome.SolverException:
+        case VcOutcome.SolverException:
           Interlocked.Increment(ref stats.SolverExceptionCount);
 
           break;
-        case VCGen.Outcome.Inconclusive:
+        case VcOutcome.Inconclusive:
           Interlocked.Increment(ref stats.InconclusiveCount);
 
           break;
-        case VCGen.Outcome.Errors:
+        case VcOutcome.Errors:
           int cnt = errors.Count(e => !e.IsAuxiliaryCexForDiagnosingTimeouts);
           Interlocked.Add(ref stats.ErrorCount, cnt);
 
@@ -1267,43 +1267,43 @@ private static void UpdateStatistics(PipelineStatistics stats, VC.VCGen.Outcome
       }
     }
 
-    private static void UpdateCachedStatistics(PipelineStatistics stats, VC.VCGen.Outcome outcome, List<Counterexample> errors) {
+    private static void UpdateCachedStatistics(PipelineStatistics stats, VcOutcome vcOutcome, List<Counterexample> errors) {
       Contract.Requires(stats != null);
 
-      switch (outcome)
+      switch (vcOutcome)
       {
         default:
           Contract.Assert(false); // unexpected outcome
           throw new cce.UnreachableException();
-        case VCGen.Outcome.ReachedBound:
+        case VcOutcome.ReachedBound:
           Interlocked.Increment(ref stats.CachedVerifiedCount);
 
           break;
-        case VCGen.Outcome.Correct:
+        case VcOutcome.Correct:
           Interlocked.Increment(ref stats.CachedVerifiedCount);
 
           break;
-        case VCGen.Outcome.TimedOut:
+        case VcOutcome.TimedOut:
           Interlocked.Increment(ref stats.CachedTimeoutCount);
 
           break;
-        case VCGen.Outcome.OutOfResource:
+        case VcOutcome.OutOfResource:
           Interlocked.Increment(ref stats.CachedOutOfResourceCount);
 
           break;
-        case VCGen.Outcome.OutOfMemory:
+        case VcOutcome.OutOfMemory:
           Interlocked.Increment(ref stats.CachedOutOfMemoryCount);
 
           break;
-        case VCGen.Outcome.SolverException:
+        case VcOutcome.SolverException:
           Interlocked.Increment(ref stats.CachedSolverExceptionCount);
 
           break;
-        case VCGen.Outcome.Inconclusive:
+        case VcOutcome.Inconclusive:
           Interlocked.Increment(ref stats.CachedInconclusiveCount);
 
           break;
-        case VCGen.Outcome.Errors:
+        case VcOutcome.Errors:
           int cnt = errors.Count(e => !e.IsAuxiliaryCexForDiagnosingTimeouts);
           Interlocked.Add(ref stats.CachedErrorCount, cnt);
 
@@ -1313,7 +1313,7 @@ private static void UpdateCachedStatistics(PipelineStatistics stats, VC.VCGen.Ou
 
     public void ProcessErrors(OutputPrinter printer,
       List<Counterexample> errors,
-      ConditionGeneration.Outcome outcome, TextWriter tw,
+      VcOutcome vcOutcome, TextWriter tw,
       ErrorReporterDelegate er, Implementation impl = null)
     {
       var implName = impl?.VerboseName;
@@ -1331,7 +1331,7 @@ public void ProcessErrors(OutputPrinter printer,
           continue;
         }
 
-        var errorInfo = error.CreateErrorInformation(outcome, Options.ForceBplErrors);
+        var errorInfo = error.CreateErrorInformation(vcOutcome, Options.ForceBplErrors);
         errorInfo.ImplementationName = implName;
 
         if (Options.XmlSink != null)
diff --git a/Source/ExecutionEngine/VerificationResult.cs b/Source/ExecutionEngine/ImplementationRunResult.cs
similarity index 75%
rename from Source/ExecutionEngine/VerificationResult.cs
rename to Source/ExecutionEngine/ImplementationRunResult.cs
index 0a685c2fd..d0169164f 100644
--- a/Source/ExecutionEngine/VerificationResult.cs
+++ b/Source/ExecutionEngine/ImplementationRunResult.cs
@@ -7,7 +7,7 @@
 
 namespace Microsoft.Boogie;
 
-public sealed class VerificationResult
+public sealed class ImplementationRunResult
 {
   private readonly Implementation implementation;
   public readonly string ProgramId;
@@ -37,20 +37,20 @@ public int ProofObligationCount
   public int ProofObligationCountBefore { get; set; }
   public int ProofObligationCountAfter { get; set; }
 
-  public ConditionGeneration.Outcome Outcome { get; set; }
+  public VcOutcome VcOutcome { get; set; }
   public List<Counterexample> Errors = new();
-  public List<VCResult> VCResults;
+  public List<VerificationRunResult> VCResults;
 
   public ErrorInformation ErrorBeforeVerification { get; set; }
 
-  public VerificationResult(Implementation implementation, string programId = null)
+  public ImplementationRunResult(Implementation implementation, string programId = null)
   {
     this.implementation = implementation;
     ProgramId = programId;
   }
 
   public ErrorInformation GetOutcomeError(ExecutionEngineOptions options) {
-    return ExecutionEngine.GetOutcomeError(options, Outcome, implementation.VerboseName, implementation.tok, MessageIfVerifies,
+    return ExecutionEngine.GetOutcomeError(options, VcOutcome, implementation.VerboseName, implementation.tok, MessageIfVerifies,
       TextWriter.Null, implementation.GetTimeLimit(options), Errors);
   }
 
@@ -62,11 +62,11 @@ public String GetOutput(OutputPrinter printer,
       printer.WriteErrorInformation(ErrorBeforeVerification, result);
     }
 
-    engine.ProcessOutcome(printer, Outcome, Errors, TimeIndication(engine.Options), stats,
+    engine.ProcessOutcome(printer, VcOutcome, Errors, TimeIndication(engine.Options), stats,
       result, implementation.GetTimeLimit(engine.Options), er, implementation.VerboseName, implementation.tok,
       MessageIfVerifies);
 
-    engine.ProcessErrors(printer, Errors, Outcome, result, er, implementation);
+    engine.ProcessErrors(printer, Errors, VcOutcome, result, er, implementation);
 
     return result.ToString();
   }
@@ -79,12 +79,12 @@ public void ProcessXml(ExecutionEngine engine) {
     lock (engine.Options.XmlSink) {
       engine.Options.XmlSink.WriteStartMethod(implementation.VerboseName, Start);
 
-      foreach (var vcResult in VCResults.OrderBy(s => (s.vcNum, s.iteration))) {
-        engine.Options.XmlSink.WriteSplit(vcResult.vcNum, vcResult.iteration, vcResult.asserts, vcResult.startTime,
-          vcResult.outcome.ToString().ToLowerInvariant(), vcResult.runTime, vcResult.resourceCount);
+      foreach (var vcResult in VCResults.OrderBy(s => (vcNum: s.VcNum, iteration: s.Iteration))) {
+        engine.Options.XmlSink.WriteSplit(vcResult.VcNum, vcResult.Iteration, vcResult.Asserts, vcResult.StartTime,
+          vcResult.Outcome.ToString().ToLowerInvariant(), vcResult.RunTime, vcResult.ResourceCount);
       }
 
-      engine.Options.XmlSink.WriteEndMethod(Outcome.ToString().ToLowerInvariant(),
+      engine.Options.XmlSink.WriteEndMethod(VcOutcome.ToString().ToLowerInvariant(),
         End, Elapsed,
         ResourceCount);
     }
diff --git a/Source/ExecutionEngine/ImplementationTask.cs b/Source/ExecutionEngine/ImplementationTask.cs
index 6badd42d0..26e385c9d 100644
--- a/Source/ExecutionEngine/ImplementationTask.cs
+++ b/Source/ExecutionEngine/ImplementationTask.cs
@@ -15,7 +15,7 @@ public interface IVerificationStatus {}
 /// <summary>
 /// Results are available
 /// </summary>
-public record Completed(VerificationResult Result) : IVerificationStatus;
+public record Completed(ImplementationRunResult Result) : IVerificationStatus;
 
 /// <summary>
 /// Scheduled to be run but waiting for resources
@@ -32,7 +32,7 @@ public record Stale : IVerificationStatus;
 /// </summary>
 public record Running : IVerificationStatus;
 
-public record BatchCompleted(Split Split, VCResult VcResult) : IVerificationStatus;
+public record BatchCompleted(Split Split, VerificationRunResult VerificationRunResult) : IVerificationStatus;
 
 public interface IImplementationTask {
   IVerificationStatus CacheStatus { get; }
diff --git a/Source/ExecutionEngine/OutputPrinter.cs b/Source/ExecutionEngine/OutputPrinter.cs
index b24301561..527fc07e8 100644
--- a/Source/ExecutionEngine/OutputPrinter.cs
+++ b/Source/ExecutionEngine/OutputPrinter.cs
@@ -14,5 +14,5 @@ public interface OutputPrinter
   void WriteTrailer(TextWriter textWriter, PipelineStatistics stats);
   void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true);
   void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null);
-  void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result);
+  void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result);
 }
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index f03417e2b..1385c03d6 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -229,16 +229,16 @@ public static void Inject(ExecutionEngine engine, Program program,
     }
 
     private void SetErrorAndAssertionChecksumsInCachedSnapshot(Implementation implementation,
-      VerificationResult result)
+      ImplementationRunResult result)
     {
-      if (result.Outcome == ConditionGeneration.Outcome.Errors && result.Errors != null &&
+      if (result.VcOutcome == VcOutcome.Errors && result.Errors != null &&
           result.Errors.Count < options.ErrorLimit)
       {
         implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex =>
           new Tuple<byte[], byte[], object>(cex.Checksum, cex.SugaredCmdChecksum, cex)));
         implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;
       }
-      else if (result.Outcome == ConditionGeneration.Outcome.Correct)
+      else if (result.VcOutcome == VcOutcome.Correct)
       {
         implementation.SetErrorChecksumToCachedError(new List<Tuple<byte[], byte[], object>>());
         implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;
@@ -690,7 +690,7 @@ public Program CachedProgram(string programId) {
     private readonly CacheItemPolicy Policy = new CacheItemPolicy
       {SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default};
 
-    public void Insert(Implementation impl, VerificationResult result)
+    public void Insert(Implementation impl, ImplementationRunResult result)
     {
       Contract.Requires(impl != null);
       Contract.Requires(result != null);
@@ -699,11 +699,11 @@ public void Insert(Implementation impl, VerificationResult result)
     }
 
 
-    public VerificationResult Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)
+    public ImplementationRunResult Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)
     {
       Contract.Requires(impl != null);
 
-      var result = Cache.Get(impl.Id) as VerificationResult;
+      var result = Cache.Get(impl.Id) as ImplementationRunResult;
       if (result == null)
       {
         priority = Priority.HIGH;
@@ -716,7 +716,7 @@ public VerificationResult Lookup(Implementation impl, bool runDiagnosticsOnTimeo
       {
         priority = Priority.LOW;
       }
-      else if (result.Outcome == ConditionGeneration.Outcome.TimedOut && runDiagnosticsOnTimeout)
+      else if (result.VcOutcome == VcOutcome.TimedOut && runDiagnosticsOnTimeout)
       {
         priority = Priority.MEDIUM;
       }
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 9620b1889..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(ProverInterface.Outcome outcome)
+    public virtual void UpdateOutcome(SolverOutcome outcome)
     {
     }
 
@@ -158,7 +158,7 @@ public override void UpdateImplementation(Implementation implementation)
       curImp = implementation;
     }
 
-    public override void UpdateOutcome(ProverInterface.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(ProverInterface.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(ProverInterface.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(ProverInterface.Outcome outcome, List<Counterexample> errors)
+    private bool IsOutcomeNotHoudini(SolverOutcome outcome, List<Counterexample> errors)
     {
       switch (outcome)
       {
-        case ProverInterface.Outcome.Valid:
+        case SolverOutcome.Valid:
           return false;
-        case ProverInterface.Outcome.Invalid:
+        case SolverOutcome.Invalid:
           Contract.Assume(errors != null);
           foreach (Counterexample error in errors)
           {
@@ -863,14 +863,14 @@ private bool IsOutcomeNotHoudini(ProverInterface.Outcome outcome, List<Counterex
     // Return true if there was at least one non-candidate error
     protected bool UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,
       Implementation implementation,
-      ProverInterface.Outcome outcome,
+      SolverOutcome outcome,
       List<Counterexample> errors)
     {
       string implName = implementation.Name;
       houdiniOutcome.implementationOutcomes.Remove(implName);
       List<Counterexample> nonCandidateErrors = new List<Counterexample>();
 
-      if (outcome == ProverInterface.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(ProverInterface.Outcome outcome,
+    protected bool UpdateAssignmentWorkList(SolverOutcome outcome,
       List<Counterexample> errors)
     {
       Contract.Assume(currentHoudiniState.Implementation != null);
@@ -945,11 +945,11 @@ protected bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome,
 
       switch (outcome)
       {
-        case ProverInterface.Outcome.Valid:
+        case SolverOutcome.Valid:
           //yeah, dequeue
           break;
 
-        case ProverInterface.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<(ProverInterface.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 (ProverInterface.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 == ProverInterface.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 == ProverInterface.Outcome.Valid)
+          if (Options.UseUnsatCoreForContractInfer && outcome == SolverOutcome.Valid)
           {
             await session.UpdateUnsatCore(proverInterface, currentHoudiniState.Assignment);
           }
@@ -1704,12 +1704,12 @@ public static void ApplyAssignment(Program prog, HoudiniOutcome outcome)
 
   public class VCGenOutcome
   {
-    public VCGen.Outcome outcome;
+    public VcOutcome VcOutcome;
     public List<Counterexample> errors;
 
-    public VCGenOutcome(ProverInterface.Outcome outcome, List<Counterexample> errors)
+    public VCGenOutcome(SolverOutcome outcome, List<Counterexample> errors)
     {
-      this.outcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
+      this.VcOutcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
       this.errors = errors;
     }
   }
@@ -1724,12 +1724,12 @@ public class HoudiniOutcome
 
     // statistics 
 
-    private int CountResults(VCGen.Outcome outcome)
+    private int CountResults(VcOutcome vcOutcome)
     {
       int outcomeCount = 0;
       foreach (VCGenOutcome verifyOutcome in implementationOutcomes.Values)
       {
-        if (verifyOutcome.outcome == outcome)
+        if (verifyOutcome.VcOutcome == vcOutcome)
         {
           outcomeCount++;
         }
@@ -1738,12 +1738,12 @@ private int CountResults(VCGen.Outcome outcome)
       return outcomeCount;
     }
 
-    private List<string> ListOutcomeMatches(VCGen.Outcome outcome)
+    private List<string> ListOutcomeMatches(VcOutcome vcOutcome)
     {
       List<string> result = new List<string>();
       foreach (KeyValuePair<string, VCGenOutcome> kvpair in implementationOutcomes)
       {
-        if (kvpair.Value.outcome == outcome)
+        if (kvpair.Value.VcOutcome == vcOutcome)
         {
           result.Add(kvpair.Key);
         }
@@ -1754,37 +1754,37 @@ private List<string> ListOutcomeMatches(VCGen.Outcome outcome)
 
     public int ErrorCount
     {
-      get { return CountResults(VCGen.Outcome.Errors); }
+      get { return CountResults(VcOutcome.Errors); }
     }
 
     public int Verified
     {
-      get { return CountResults(VCGen.Outcome.Correct); }
+      get { return CountResults(VcOutcome.Correct); }
     }
 
     public int Inconclusives
     {
-      get { return CountResults(VCGen.Outcome.Inconclusive); }
+      get { return CountResults(VcOutcome.Inconclusive); }
     }
 
     public int TimeOuts
     {
-      get { return CountResults(VCGen.Outcome.TimedOut); }
+      get { return CountResults(VcOutcome.TimedOut); }
     }
 
     public List<string> ListOfTimeouts
     {
-      get { return ListOutcomeMatches(VCGen.Outcome.TimedOut); }
+      get { return ListOutcomeMatches(VcOutcome.TimedOut); }
     }
 
     public List<string> ListOfInconclusives
     {
-      get { return ListOutcomeMatches(VCGen.Outcome.Inconclusive); }
+      get { return ListOutcomeMatches(VcOutcome.Inconclusive); }
     }
 
     public List<string> ListOfErrors
     {
-      get { return ListOutcomeMatches(VCGen.Outcome.Errors); }
+      get { return ListOutcomeMatches(VcOutcome.Errors); }
     }
   }
 }
\ No newline at end of file
diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs
index 7603402d2..5c1032115 100644
--- a/Source/Houdini/HoudiniSession.cs
+++ b/Source/Houdini/HoudiniSession.cs
@@ -129,7 +129,7 @@ public class HoudiniStatistics
     public HashSet<TrackedNodeComponent> CoveredElements { get; } = new();
     private VCExpr conjecture;
     private ProverInterface.ErrorHandler handler;
-    ConditionGeneration.VerificationResultCollector collector;
+    VerificationResultCollector collector;
     HashSet<Variable> unsatCoreSet;
     HashSet<Variable> houdiniConstants;
     public HashSet<Variable> houdiniAssertConstants;
@@ -156,14 +156,14 @@ 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;
       this.Description = impl.Name;
       this.houdini = houdini;
       this.stats = stats;
-      collector = new ConditionGeneration.VerificationResultCollector(houdini.Options);
+      collector = new VerificationResultCollector(houdini.Options);
       collector.OnProgress?.Invoke("HdnVCGen", 0, 0, 0.0);
 
       vcgen.ConvertCFG2DAG(run, taskID: taskID);
@@ -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<(ProverInterface.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 = ProverInterface.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 == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory ||
-            outcome == ProverInterface.Outcome.OutOfResource || outcome == ProverInterface.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 == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory ||
-            outcome == ProverInterface.Outcome.OutOfResource || outcome == ProverInterface.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 == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory ||
-          outcome == ProverInterface.Outcome.OutOfResource || outcome == ProverInterface.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));
       }
 
-      (ProverInterface.Outcome tmp, var unsatCore) = await proverInterface.CheckAssumptions(assumptionExprs, handler, CancellationToken.None);
-      System.Diagnostics.Debug.Assert(tmp == ProverInterface.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/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs
index e50e23b73..ce2cea26d 100644
--- a/Source/Houdini/StagedHoudini.cs
+++ b/Source/Houdini/StagedHoudini.cs
@@ -6,6 +6,7 @@
 using System.Threading.Tasks;
 using System.Threading;
 using Microsoft.Boogie.GraphUtil;
+using VC;
 
 namespace Microsoft.Boogie.Houdini
 {
@@ -308,8 +309,8 @@ private void EmitProgram(string filename)
 
     private static VCGenOutcome ChooseOutcome(VCGenOutcome o1, VCGenOutcome o2)
     {
-      var vcOutcome1 = o1.outcome;
-      var vcOutcome2 = o2.outcome;
+      var vcOutcome1 = o1.VcOutcome;
+      var vcOutcome2 = o2.VcOutcome;
 
       if (vcOutcome1 == vcOutcome2)
       {
@@ -317,34 +318,34 @@ private static VCGenOutcome ChooseOutcome(VCGenOutcome o1, VCGenOutcome o2)
       }
 
       // Errors trump everything else
-      if (vcOutcome1 == VC.ConditionGeneration.Outcome.Errors)
+      if (vcOutcome1 == VcOutcome.Errors)
       {
         return o1;
       }
 
-      if (vcOutcome2 == VC.ConditionGeneration.Outcome.Errors)
+      if (vcOutcome2 == VcOutcome.Errors)
       {
         return o2;
       }
 
       // If one outcome is Correct, return the other in case it is "worse"
-      if (vcOutcome1 == VC.ConditionGeneration.Outcome.Correct)
+      if (vcOutcome1 == VcOutcome.Correct)
       {
         return o2;
       }
 
-      if (vcOutcome2 == VC.ConditionGeneration.Outcome.Correct)
+      if (vcOutcome2 == VcOutcome.Correct)
       {
         return o1;
       }
 
       // Neither outcome is correct, so if one outcome is ReachedBound, return the other in case it is "worse"
-      if (vcOutcome1 == VC.ConditionGeneration.Outcome.ReachedBound)
+      if (vcOutcome1 == VcOutcome.ReachedBound)
       {
         return o2;
       }
 
-      if (vcOutcome2 == VC.ConditionGeneration.Outcome.ReachedBound)
+      if (vcOutcome2 == VcOutcome.ReachedBound)
       {
         return o1;
       }
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index bad3f03f0..145010769 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -90,17 +90,6 @@ public static ProverInterface CreateProver(SMTLibOptions libOptions, Program pro
     return libOptions.TheProverFactory.SpawnProver(libOptions, options, ctx);
   }
 
-  public enum Outcome
-  {
-    Valid,
-    Invalid,
-    TimeOut,
-    OutOfMemory,
-    OutOfResource,
-    Undetermined,
-    Bounded
-  }
-
   public readonly ISet<VCExprVar> NamedAssumes = new HashSet<VCExprVar>();
 
   public class ErrorHandler
@@ -123,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));
     }
@@ -168,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)
   {
@@ -243,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();
@@ -305,6 +294,18 @@ public virtual void AssertNamed(VCExpr vc, bool polarity, string name)
 
   public abstract Task GoBackToIdle();
 }
+
+public enum SolverOutcome
+{
+  Valid,
+  Invalid,
+  TimeOut,
+  OutOfMemory,
+  OutOfResource,
+  Undetermined,
+  Bounded
+}
+
 public class UnexpectedProverOutputException : ProverException
 {
   public UnexpectedProverOutputException(string s)
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 26ee5dbd3..7eda7869a 100644
--- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
+++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
@@ -71,7 +71,7 @@ procedure Second(y: int)
     Assert.NotNull(tasks[0].Implementation);
     var result1 = await tasks[0].TryRun()!.ToTask();
     var verificationResult1 = ((Completed)result1).Result;
-    Assert.AreEqual(ConditionGeneration.Outcome.Errors, verificationResult1.Outcome);
+    Assert.AreEqual(VcOutcome.Errors, verificationResult1.VcOutcome);
     Assert.AreEqual(true, verificationResult1.Errors[0].Model.ModelHasStatesAlready);
 
     Assert.IsTrue(tasks[1].IsIdle);
@@ -80,7 +80,7 @@ procedure Second(y: int)
     var result2 = await runningStates.ToTask();
     Assert.IsTrue(tasks[1].IsIdle);
     var verificationResult2 = ((Completed)result2).Result;
-    Assert.AreEqual(ConditionGeneration.Outcome.Correct, verificationResult2.Outcome);
+    Assert.AreEqual(VcOutcome.Correct, verificationResult2.VcOutcome);
   }
 
   [Test]
@@ -340,20 +340,20 @@ public async Task StatusTest() {
     
     var tasks2 = engine.GetImplementationTasks(program);
     Assert.True(tasks2[0].CacheStatus is Completed);
-    Assert.AreEqual(ConditionGeneration.Outcome.Errors, ((Completed)tasks2[0].CacheStatus).Result.Outcome);
+    Assert.AreEqual(VcOutcome.Errors, ((Completed)tasks2[0].CacheStatus).Result.VcOutcome);
 
     Assert.True(tasks2[1].CacheStatus is Completed);
-    Assert.AreEqual(ConditionGeneration.Outcome.Correct, ((Completed)tasks2[1].CacheStatus).Result.Outcome);
+    Assert.AreEqual(VcOutcome.Correct, ((Completed)tasks2[1].CacheStatus).Result.VcOutcome);
     
     var batchResult = (BatchCompleted) statusList[2].Item2;
     
-    var assertion = batchResult.VcResult.asserts[0];
-    batchResult.VcResult.ComputePerAssertOutcomes(out var perAssertOutcome, out var perAssertCounterExamples);
+    var assertion = batchResult.VerificationRunResult.Asserts[0];
+    batchResult.VerificationRunResult.ComputePerAssertOutcomes(out var perAssertOutcome, out var perAssertCounterExamples);
     Assert.Contains(assertion, perAssertOutcome.Keys);
     Assert.Contains(assertion, perAssertCounterExamples.Keys);
     var outcomeAssertion = perAssertOutcome[assertion];
     var counterExampleAssertion = perAssertCounterExamples[assertion];
-    Assert.AreEqual(ProverInterface.Outcome.Invalid, outcomeAssertion);
+    Assert.AreEqual(SolverOutcome.Invalid, outcomeAssertion);
     Assert.AreEqual(true, counterExampleAssertion is AssertCounterexample);
     var assertCounterexample = (AssertCounterexample)counterExampleAssertion;
     Assert.AreEqual(assertCounterexample.FailingAssert, assertion);
@@ -374,10 +374,10 @@ public async Task SolverCrash()
     options.VcsCores = 1;
 
     var outcome1 = await executionEngine.GetImplementationTasks(terminatingProgram)[0].TryRun()!.ToTask();
-    Assert.IsTrue(outcome1 is Completed completed && completed.Result.Outcome == ConditionGeneration.Outcome.Inconclusive);
+    Assert.IsTrue(outcome1 is Completed completed && completed.Result.VcOutcome == VcOutcome.Inconclusive);
     options.CreateSolver = (_ ,_ ) => new UnsatSolver();
     var outcome2 = await executionEngine.GetImplementationTasks(terminatingProgram)[0].TryRun()!.ToTask();
-    Assert.IsTrue(outcome2 is Completed completed2 && completed2.Result.Outcome == ConditionGeneration.Outcome.Correct);
+    Assert.IsTrue(outcome2 is Completed completed2 && completed2.Result.VcOutcome == VcOutcome.Correct);
   }
 
   [Test]
diff --git a/Source/UnitTests/ExecutionEngineTests/NullPrinter.cs b/Source/UnitTests/ExecutionEngineTests/NullPrinter.cs
index 99175bb0a..d14791b30 100644
--- a/Source/UnitTests/ExecutionEngineTests/NullPrinter.cs
+++ b/Source/UnitTests/ExecutionEngineTests/NullPrinter.cs
@@ -30,7 +30,7 @@ public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, boo
   public void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) {
   }
 
-  public void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result)
+  public void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result)
   {
   }
 }
diff --git a/Source/VCGeneration/BlockListComparer.cs b/Source/VCGeneration/BlockListComparer.cs
new file mode 100644
index 000000000..3df87811c
--- /dev/null
+++ b/Source/VCGeneration/BlockListComparer.cs
@@ -0,0 +1,29 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using Microsoft.Boogie;
+
+namespace VC;
+
+class BlockListComparer : IEqualityComparer<List<Block>>
+{
+  public bool Equals(List<Block> x, List<Block> y)
+  {
+    return x == y || x.SequenceEqual(y);
+  }
+
+  public int GetHashCode(List<Block> obj)
+  {
+    int h = 0;
+    Contract.Assume(obj != null);
+    foreach (var b in obj)
+    {
+      if (b != null)
+      {
+        h += b.GetHashCode();
+      }
+    }
+
+    return h;
+  }
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/BlockStats.cs b/Source/VCGeneration/BlockStats.cs
new file mode 100644
index 000000000..eba08b349
--- /dev/null
+++ b/Source/VCGeneration/BlockStats.cs
@@ -0,0 +1,40 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
+
+namespace VC;
+
+class BlockStats
+{
+  public bool bigBlock;
+  public int id;
+  public double assertionCost;
+  public double assumptionCost; // before multiplier
+  public double incomingPaths;
+
+  public List<Block> /*!>!*/
+    virtualSuccessors = new List<Block>();
+
+  public List<Block> /*!>!*/
+    virtualPredecessors = new List<Block>();
+
+  public HashSet<Block> reachableBlocks;
+  public readonly Block block;
+
+  [ContractInvariantMethod]
+  void ObjectInvariant()
+  {
+    Contract.Invariant(cce.NonNullElements(virtualSuccessors));
+    Contract.Invariant(cce.NonNullElements(virtualPredecessors));
+    Contract.Invariant(block != null);
+  }
+
+
+  public BlockStats(Block b, int i)
+  {
+    Contract.Requires(b != null);
+    block = b;
+    assertionCost = -1;
+    id = i;
+  }
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs
new file mode 100644
index 000000000..89f17aac7
--- /dev/null
+++ b/Source/VCGeneration/BlockTransformations.cs
@@ -0,0 +1,64 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using Microsoft.Boogie;
+
+namespace VCGeneration;
+
+public static class BlockTransformations
+{
+    public static List<Block> PostProcess(List<Block> blocks)
+    {
+      void DeleteFalseGotos (Block b)
+      {
+        var firstFalseIdx = b.Cmds.FindIndex(IsAssumeFalse);
+        if (firstFalseIdx != -1)
+        {
+          b.Cmds = b.Cmds.Take(firstFalseIdx + 1).ToList();
+          b.TransferCmd = (b.TransferCmd is GotoCmd) ? new ReturnCmd(b.tok) : b.TransferCmd;
+        }
+
+        return;
+
+        bool IsAssumeFalse (Cmd c) { return c is AssumeCmd ac && ac.Expr is LiteralExpr le && !le.asBool; }
+      }
+
+      bool ContainsAssert(Block b)
+      {
+        return b.Cmds.Exists(IsNonTrivialAssert);
+        bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); }
+      }
+
+      blocks.ForEach(DeleteFalseGotos); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously
+      var todo = new Stack<Block>();
+      var peeked = new HashSet<Block>();
+      var interestingBlocks = new HashSet<Block>();
+      todo.Push(blocks[0]);
+      while(todo.Any())
+      {
+        var currentBlock = todo.Peek();
+        var pop = peeked.Contains(currentBlock);
+        peeked.Add(currentBlock);
+        var interesting = false;
+        var exit = currentBlock.TransferCmd as GotoCmd;
+        if (exit != null && !pop) {
+          exit.labelTargets.ForEach(b => todo.Push(b));
+        } else if (exit != null) {
+          Contract.Assert(pop);
+          var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList());
+          currentBlock.TransferCmd = gtc;
+          interesting = interesting || gtc.labelTargets.Count() != 0;
+        }
+        if (pop)
+        {
+          interesting = interesting || ContainsAssert(currentBlock);
+          if (interesting) {
+            interestingBlocks.Add(currentBlock);
+          }
+          todo.Pop();
+        }
+      }
+      interestingBlocks.Add(blocks[0]); // must not be empty
+      return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders.
+    }
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs
index f5f8c2f8d..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 ProverInterface.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 ProverInterface.Outcome.Valid:
+        case SolverOutcome.Valid:
           thmProver.LogComment("Valid");
           break;
-        case ProverInterface.Outcome.Invalid:
+        case SolverOutcome.Invalid:
           thmProver.LogComment("Invalid");
           break;
-        case ProverInterface.Outcome.TimeOut:
+        case SolverOutcome.TimeOut:
           thmProver.LogComment("Timed out");
           break;
-        case ProverInterface.Outcome.OutOfResource:
+        case SolverOutcome.OutOfResource:
           thmProver.LogComment("Out of resource");
           break;
-        case ProverInterface.Outcome.OutOfMemory:
+        case SolverOutcome.OutOfMemory:
           thmProver.LogComment("Out of memory");
           break;
-        case ProverInterface.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 ProverInterface.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
new file mode 100644
index 000000000..74daf7195
--- /dev/null
+++ b/Source/VCGeneration/CommandTransformations.cs
@@ -0,0 +1,17 @@
+using Microsoft.Boogie;
+using VC;
+
+namespace VCGeneration;
+
+public class CommandTransformations
+{
+  public static Cmd AssertIntoAssume(VCGenOptions options, Cmd c)
+  {
+    if (c is AssertCmd assrt)
+    {
+      return VerificationConditionGenerator.AssertTurnedIntoAssume(options, assrt);
+    }
+
+    return c;
+  }
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index d9d900377..4a8b93924 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1,7 +1,6 @@
 using System;
 using System.Linq;
 using System.Collections;
-using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.Diagnostics;
 using System.Threading;
@@ -27,8 +26,8 @@ public VCGenException(string s)
   [ContractClassFor(typeof(ConditionGeneration))]
   public abstract class ConditionGenerationContracts : ConditionGeneration
   {
-    public override Task<Outcome> VerifyImplementation(ImplementationRun run, VerifierCallback callback,
-      CancellationToken cancellationToken, IObserver<(Split split, VCResult vcResult)> batchCompletedObserver)
+    public override Task<VcOutcome> VerifyImplementation(ImplementationRun run, VerifierCallback callback,
+      CancellationToken cancellationToken, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver)
     {
       Contract.Requires(run != null);
       Contract.Requires(callback != null);
@@ -45,37 +44,25 @@ public ConditionGenerationContracts(Program program, CheckerPool checkerPool)
   [ContractClass(typeof(ConditionGenerationContracts))]
   public abstract class ConditionGeneration : IDisposable
   {
-    public enum Outcome
-    {
-      Correct,
-      Errors,
-      TimedOut,
-      OutOfResource,
-      OutOfMemory,
-      Inconclusive,
-      ReachedBound,
-      SolverException
-    }
-
-    public static Outcome ProverInterfaceOutcomeToConditionGenerationOutcome(ProverInterface.Outcome outcome)
+    public static VcOutcome ProverInterfaceOutcomeToConditionGenerationOutcome(Microsoft.Boogie.SolverOutcome outcome)
     {
       switch (outcome)
       {
-        case ProverInterface.Outcome.Invalid:
-          return Outcome.Errors;
-        case ProverInterface.Outcome.OutOfMemory:
-          return Outcome.OutOfMemory;
-        case ProverInterface.Outcome.TimeOut:
-          return Outcome.TimedOut;
-        case ProverInterface.Outcome.OutOfResource:
-          return Outcome.OutOfResource;
-        case ProverInterface.Outcome.Undetermined:
-          return Outcome.Inconclusive;
-        case ProverInterface.Outcome.Valid:
-          return Outcome.Correct;
+        case Microsoft.Boogie.SolverOutcome.Invalid:
+          return VcOutcome.Errors;
+        case Microsoft.Boogie.SolverOutcome.OutOfMemory:
+          return VcOutcome.OutOfMemory;
+        case Microsoft.Boogie.SolverOutcome.TimeOut:
+          return VcOutcome.TimedOut;
+        case Microsoft.Boogie.SolverOutcome.OutOfResource:
+          return VcOutcome.OutOfResource;
+        case Microsoft.Boogie.SolverOutcome.Undetermined:
+          return VcOutcome.Inconclusive;
+        case Microsoft.Boogie.SolverOutcome.Valid:
+          return VcOutcome.Correct;
       }
 
-      return Outcome.Inconclusive; // unreachable but the stupid compiler does not understand
+      return VcOutcome.Inconclusive; // unreachable but the stupid compiler does not understand
     }
 
     [ContractInvariantMethod]
@@ -120,8 +107,8 @@ public ConditionGeneration(Program program, CheckerPool checkerPool)
     /// <param name="batchCompletedObserver"></param>
     /// <param name="cancellationToken"></param>
     /// <param name="impl"></param>
-    public async Task<(Outcome, List<Counterexample> errors, List<VCResult> vcResults)> VerifyImplementation(
-      ImplementationRun run, IObserver<(Split split, VCResult vcResult)> batchCompletedObserver,
+    public async Task<(VcOutcome, List<Counterexample> errors, List<VerificationRunResult> vcResults)> VerifyImplementation(
+      ImplementationRun run, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver,
       CancellationToken cancellationToken)
     {
       Contract.Requires(run != null);
@@ -130,21 +117,21 @@ public ConditionGeneration(Program program, CheckerPool checkerPool)
       Helpers.ExtraTraceInformation(Options, "Starting implementation verification");
 
       var collector = new VerificationResultCollector(Options);
-      Outcome outcome = await VerifyImplementation(run, collector, cancellationToken, batchCompletedObserver);
+      VcOutcome vcOutcome = await VerifyImplementation(run, collector, cancellationToken, batchCompletedObserver);
       var /*?*/ errors = new List<Counterexample>();
-      if (outcome == Outcome.Errors || outcome == Outcome.TimedOut || outcome == Outcome.OutOfMemory ||
-          outcome == Outcome.OutOfResource) {
+      if (vcOutcome == VcOutcome.Errors || vcOutcome == VcOutcome.TimedOut || vcOutcome == VcOutcome.OutOfMemory ||
+          vcOutcome == VcOutcome.OutOfResource) {
         errors = collector.examples.ToList();
       }
 
       Helpers.ExtraTraceInformation(Options, "Finished implementation verification");
-      return (outcome, errors, collector.vcResults.ToList());
+      return (vcOutcome, errors, collector.vcResults.ToList());
     }
 
     private VCGenOptions Options => CheckerPool.Options;
 
-    public abstract Task<Outcome> VerifyImplementation(ImplementationRun run, VerifierCallback callback,
-      CancellationToken cancellationToken, IObserver<(Split split, VCResult vcResult)> batchCompletedObserver);
+    public abstract Task<VcOutcome> VerifyImplementation(ImplementationRun run, VerifierCallback callback,
+      CancellationToken cancellationToken, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver);
 
     /////////////////////////////////// Common Methods and Classes //////////////////////////////////////////
 
@@ -523,46 +510,6 @@ public virtual void Close()
     }
 
 
-    public class VerificationResultCollector : VerifierCallback
-    {
-      private readonly VCGenOptions options;
-
-      public VerificationResultCollector(VCGenOptions options) : base(options.PrintProverWarnings)
-      {
-        this.options = options;
-      }
-
-      [ContractInvariantMethod]
-      void ObjectInvariant()
-      {
-        Contract.Invariant(cce.NonNullElements(examples));
-        Contract.Invariant(cce.NonNullElements(vcResults));
-      }
-
-      public readonly ConcurrentQueue<Counterexample> examples = new();
-      public readonly ConcurrentQueue<VCResult> vcResults = new();
-
-      public override void OnCounterexample(Counterexample ce, string /*?*/ reason)
-      {
-        //Contract.Requires(ce != null);
-        ce.InitializeModelStates();
-        examples.Enqueue(ce);
-      }
-
-      public override void OnUnreachableCode(ImplementationRun run)
-      {
-        //Contract.Requires(impl != null);
-        run.OutputWriter.WriteLine("found unreachable code:");
-        EmitImpl(options, run, false);
-        // TODO report error about next to last in seq
-      }
-
-      public override void OnVCResult(VCResult result)
-      {
-        vcResults.Enqueue(result);
-      }
-    }
-
     public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool printDesugarings)
     {
       var impl = run.Implementation;
@@ -1662,6 +1609,18 @@ protected virtual void Dispose(bool disposing)
     }
   }
 
+  public enum VcOutcome
+  {
+    Correct,
+    Errors,
+    TimedOut,
+    OutOfResource,
+    OutOfMemory,
+    Inconclusive,
+    ReachedBound,
+    SolverException
+  }
+
   public record ImplementationRun(Implementation Implementation, TextWriter OutputWriter) {
 
   }
diff --git a/Source/VCGeneration/Counterexample.cs b/Source/VCGeneration/Counterexample.cs
index e48d0c1fa..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);
@@ -388,14 +388,14 @@ public Model.Element GetModelValue(Variable v)
 
     public abstract int GetLocation();
 
-    public ErrorInformation CreateErrorInformation(ConditionGeneration.Outcome outcome, bool forceBplErrors)
+    public ErrorInformation CreateErrorInformation(VcOutcome vcOutcome, bool forceBplErrors)
     {
       ErrorInformation errorInfo;
-      var cause = outcome switch {
-        VCGen.Outcome.TimedOut => "Timed out on",
-        VCGen.Outcome.OutOfMemory => "Out of memory on",
-        VCGen.Outcome.SolverException => "Solver exception on",
-        VCGen.Outcome.OutOfResource => "Out of resource on",
+      var cause = vcOutcome switch {
+        VcOutcome.TimedOut => "Timed out on",
+        VcOutcome.OutOfMemory => "Out of memory on",
+        VcOutcome.SolverException => "Solver exception on",
+        VcOutcome.OutOfResource => "Out of resource on",
         _ => "Error"
       };
 
@@ -766,7 +766,7 @@ public virtual void OnWarning(CoreOptions options, string msg)
       }
     }
 
-    public virtual void OnVCResult(VCResult result)
+    public virtual void OnVCResult(VerificationRunResult result)
     {
       Contract.Requires(result != null);
     }
diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs
new file mode 100644
index 000000000..72c3c76c8
--- /dev/null
+++ b/Source/VCGeneration/FocusAttribute.cs
@@ -0,0 +1,139 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using Microsoft.Boogie;
+using VC;
+using Block = Microsoft.Boogie.Block;
+using Cmd = Microsoft.Boogie.Cmd;
+using PredicateCmd = Microsoft.Boogie.PredicateCmd;
+using QKeyValue = Microsoft.Boogie.QKeyValue;
+using ReturnCmd = Microsoft.Boogie.ReturnCmd;
+using TransferCmd = Microsoft.Boogie.TransferCmd;
+using VCGenOptions = Microsoft.Boogie.VCGenOptions;
+
+namespace VCGeneration;
+
+public static class FocusAttribute
+{
+  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");
+    }
+
+    List<Block> GetFocusBlocks(List<Block> blocks) {
+      return blocks.Where(blk => blk.Cmds.Any(c => IsFocusCmd(c))).ToList();
+    }
+
+    var impl = run.Implementation;
+    var dag = Program.GraphFromImpl(impl);
+    var topoSorted = dag.TopologicalSort().ToList();
+    // By default, we process the foci in a top-down fashion, i.e., in the topological order.
+    // If the user sets the RelaxFocus flag, we use the reverse (topological) order.
+    var focusBlocks = GetFocusBlocks(topoSorted);
+    if (par.CheckerPool.Options.RelaxFocus) {
+      focusBlocks.Reverse();
+    }
+    if (!focusBlocks.Any()) {
+      var f = new List<Split>();
+      f.Add(new Split(options, impl.Blocks, gotoCmdOrigins, par, run));
+      return f;
+    }
+    // finds all the blocks dominated by focusBlock in the subgraph
+    // which only contains vertices of subgraph.
+    HashSet<Block> DominatedBlocks(Block focusBlock, IEnumerable<Block> subgraph)
+    {
+      var dominators = new Dictionary<Block, HashSet<Block>>();
+      var todo = new Queue<Block>();
+      foreach (var b in topoSorted.Where(blk => subgraph.Contains(blk)))
+      {
+        var s = new HashSet<Block>();
+        var pred = b.Predecessors.Where(subgraph.Contains).ToList();
+        if (pred.Count != 0)
+        {
+          s.UnionWith(dominators[pred[0]]);
+          pred.ForEach(blk => s.IntersectWith(dominators[blk]));
+        }
+        s.Add(b);
+        dominators[b] = s;
+      }
+      return subgraph.Where(blk => dominators[blk].Contains(focusBlock)).ToHashSet();
+    }
+
+    Cmd DisableSplits(Cmd c)
+    {
+      if (c is PredicateCmd pc)
+      {
+        for (var kv = pc.Attributes; kv != null; kv = kv.Next)
+        {
+          if (kv.Key == "split")
+          {
+            kv.AddParam(new LiteralExpr(Token.NoToken, false));
+          }
+        }
+      }
+      return c;
+    }
+
+    var Ancestors = new Dictionary<Block, HashSet<Block>>();
+    var Descendants = new Dictionary<Block, HashSet<Block>>();
+    focusBlocks.ForEach(fb => Ancestors[fb] = dag.ComputeReachability(fb, false).ToHashSet());
+    focusBlocks.ForEach(fb => Descendants[fb] = dag.ComputeReachability(fb, true).ToHashSet());
+    var s = new List<Split>();
+    var duplicator = new Duplicator();
+    void FocusRec(int focusIdx, IEnumerable<Block> blocks, IEnumerable<Block> freeBlocks)
+    {
+      if (focusIdx == focusBlocks.Count())
+      {
+        // it is important for l to be consistent with reverse topological order.
+        var l = dag.TopologicalSort().Where(blk => blocks.Contains(blk)).Reverse();
+        // assert that the root block, impl.Blocks[0], is in l
+        Contract.Assert(l.ElementAt(l.Count() - 1) == impl.Blocks[0]);
+        var newBlocks = new List<Block>();
+        var oldToNewBlockMap = new Dictionary<Block, Block>(blocks.Count());
+        foreach (Block b in l)
+        {
+          var newBlock = (Block)duplicator.Visit(b);
+          newBlocks.Add(newBlock);
+          oldToNewBlockMap[b] = newBlock;
+          // freeBlocks consist of the predecessors of the relevant foci.
+          // Their assertions turn into assumes and any splits inside them are disabled.
+          if(freeBlocks.Contains(b))
+          {
+            newBlock.Cmds = b.Cmds.Select(c => CommandTransformations.AssertIntoAssume(options, c)).Select(c => DisableSplits(c)).ToList();
+          }
+          if (b.TransferCmd is GotoCmd gtc)
+          {
+            var targets = gtc.labelTargets.Where(blk => blocks.Contains(blk));
+            newBlock.TransferCmd = new GotoCmd(gtc.tok,
+                                          targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(),
+                                          targets.Select(blk => oldToNewBlockMap[blk]).ToList());
+          }
+        }
+        newBlocks.Reverse();
+        Contract.Assert(newBlocks[0] == oldToNewBlockMap[impl.Blocks[0]]);
+        s.Add(new Split(options, BlockTransformations.PostProcess(newBlocks), gotoCmdOrigins, par, run));
+      }
+      else if (!blocks.Contains(focusBlocks[focusIdx])
+                || freeBlocks.Contains(focusBlocks[focusIdx]))
+      {
+        FocusRec(focusIdx + 1, blocks, freeBlocks);
+      }
+      else
+      {
+        var b = focusBlocks[focusIdx]; // assert b in blocks
+        var dominatedBlocks = DominatedBlocks(b, blocks);
+        // the first part takes all blocks except the ones dominated by the focus block
+        FocusRec(focusIdx + 1, blocks.Where(blk => !dominatedBlocks.Contains(blk)), freeBlocks);
+        var ancestors = Ancestors[b];
+        ancestors.Remove(b);
+        var descendants = Descendants[b];
+        // the other part takes all the ancestors, the focus block, and the descendants.
+        FocusRec(focusIdx + 1, ancestors.Union(descendants).Intersect(blocks), ancestors.Union(freeBlocks));
+      }
+    }
+
+    FocusRec(0, impl.Blocks, new List<Block>());
+    return s;
+  }
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs
new file mode 100644
index 000000000..5646d71fa
--- /dev/null
+++ b/Source/VCGeneration/ManualSplitFinder.cs
@@ -0,0 +1,167 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using Microsoft.Boogie;
+using VC;
+
+namespace VCGeneration;
+
+public static class ManualSplitFinder
+{
+  
+  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();
+    return splits;
+  }
+  
+  public static List<Split> FindManualSplits(Split initialSplit, bool splitOnEveryAssert)
+  {
+    Contract.Requires(initialSplit.Implementation != null);
+    Contract.Ensures(Contract.Result<List<Split>>() == null || cce.NonNullElements(Contract.Result<List<Split>>()));
+
+    var splitPoints = new Dictionary<Block, int>();
+    foreach (var b in initialSplit.Blocks)
+    {
+      foreach (Cmd c in b.Cmds)
+      {
+        var p = c as PredicateCmd;
+        if (ShouldSplitHere(c, splitOnEveryAssert))
+        {
+          splitPoints.TryGetValue(b, out var count);
+          splitPoints[b] = count + 1;
+        }
+      }
+    }
+    var splits = new List<Split>();
+    if (!splitPoints.Any())
+    {
+      splits.Add(initialSplit);
+    }
+    else
+    {
+      Block entryPoint = initialSplit.Blocks[0];
+      var blockAssignments = PickBlocksToVerify(initialSplit.Blocks, splitPoints);
+      var entryBlockHasSplit = splitPoints.Keys.Contains(entryPoint);
+      var baseSplitBlocks = BlockTransformations.PostProcess(DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert));
+      splits.Add(new Split(initialSplit.Options, baseSplitBlocks, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run));
+      foreach (KeyValuePair<Block, int> pair in splitPoints)
+      {
+        for (int i = 0; i < pair.Value; i++)
+        {
+          bool lastSplitInBlock = i == pair.Value - 1;
+          var newBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, i, pair.Key, lastSplitInBlock, splitOnEveryAssert);
+          splits.Add(new Split(initialSplit.Options, BlockTransformations.PostProcess(newBlocks), initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run)); // REVIEW: Does gotoCmdOrigins need to be changed at all?
+        }
+      }
+    }
+    return splits;
+  }
+
+  private static bool ShouldSplitHere(Cmd c, bool splitOnEveryAssert) {
+    return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "split_here")
+           || c is AssertCmd && splitOnEveryAssert;
+  }
+  
+
+  // Verify b with the last split in blockAssignments[b]
+
+  private static Dictionary<Block, Block> PickBlocksToVerify (List<Block> blocks, Dictionary<Block, int> splitPoints)
+  {
+    var todo = new Stack<Block>();
+    var blockAssignments = new Dictionary<Block, Block>();
+    var immediateDominator = (Program.GraphFromBlocks(blocks)).ImmediateDominator();
+    todo.Push(blocks[0]);
+    while(todo.Count > 0)
+    {
+      var currentBlock = todo.Pop();
+      if (blockAssignments.Keys.Contains(currentBlock))
+      {
+        continue;
+      }
+      else if (immediateDominator[currentBlock] == currentBlock) // if the currentBlock doesn't have a predecessor.
+      {
+        blockAssignments[currentBlock] = currentBlock;
+      }
+      else if (splitPoints.Keys.Contains(immediateDominator[currentBlock])) // if the currentBlock's dominator has a split then it will be associated with that split
+      {
+        blockAssignments[currentBlock] = immediateDominator[currentBlock];
+      }
+      else
+      {
+        Contract.Assert(blockAssignments.Keys.Contains(immediateDominator[currentBlock]));
+        blockAssignments[currentBlock] = blockAssignments[immediateDominator[currentBlock]];
+      }
+      if (currentBlock.TransferCmd is GotoCmd exit)
+      {
+        exit.labelTargets.ForEach(blk => todo.Push(blk));
+      }
+    }
+    return blockAssignments;
+  }
+
+  private static List<Block> DoPreAssignedManualSplit(VCGenOptions options, List<Block> blocks, Dictionary<Block, Block> blockAssignments, int splitNumberWithinBlock,
+    Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert)
+  {
+    var newBlocks = new List<Block>(blocks.Count()); // Copies of the original blocks
+    var duplicator = new Duplicator();
+    var oldToNewBlockMap = new Dictionary<Block, Block>(blocks.Count()); // Maps original blocks to their new copies in newBlocks
+    foreach (var currentBlock in blocks)
+    {
+      var newBlock = (Block)duplicator.VisitBlock(currentBlock);
+      oldToNewBlockMap[currentBlock] = newBlock;
+      newBlocks.Add(newBlock);
+      if (currentBlock == containingBlock)
+      {
+        var newCmds = new List<Cmd>();
+        var splitCount = -1;
+        var verify = splitCount == splitNumberWithinBlock;
+        foreach (Cmd c in currentBlock.Cmds)
+        {
+          if (ShouldSplitHere(c, splitOnEveryAssert))
+          {
+            splitCount++;
+            verify = splitCount == splitNumberWithinBlock;
+          }
+          newCmds.Add(verify ? c : CommandTransformations.AssertIntoAssume(options, c));
+        }
+        newBlock.Cmds = newCmds;
+      }
+      else if (lastSplitInBlock && blockAssignments[currentBlock] == containingBlock)
+      {
+        var verify = true;
+        var newCmds = new List<Cmd>();
+        foreach(Cmd c in currentBlock.Cmds) {
+          verify = !ShouldSplitHere(c, splitOnEveryAssert) && verify;
+          newCmds.Add(verify ? c : CommandTransformations.AssertIntoAssume(options, c));
+        }
+        newBlock.Cmds = newCmds;
+      }
+      else
+      {
+        newBlock.Cmds = currentBlock.Cmds.Select<Cmd, Cmd>(x => CommandTransformations.AssertIntoAssume(options, x)).ToList();
+      }
+    }
+    // Patch the edges between the new blocks
+    foreach (var oldBlock in blocks)
+    {
+      if (oldBlock.TransferCmd is ReturnCmd)
+      {
+        continue;
+      }
+
+      var gotoCmd = (GotoCmd)oldBlock.TransferCmd;
+      var newLabelTargets = new List<Block>(gotoCmd.labelTargets.Count());
+      var newLabelNames = new List<string>(gotoCmd.labelTargets.Count());
+      foreach (var target in gotoCmd.labelTargets)
+      {
+        newLabelTargets.Add(oldToNewBlockMap[target]);
+        newLabelNames.Add(oldToNewBlockMap[target].Label);
+      }
+
+      oldToNewBlockMap[oldBlock].TransferCmd = new GotoCmd(gotoCmd.tok, newLabelNames, newLabelTargets);
+    }
+    return newBlocks;
+  }
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs
index f449cce68..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);
 
-    ProverInterface.Outcome outcome = ProverInterface.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 == ProverInterface.Outcome.Valid
+        outcome == SolverOutcome.Valid
           ? "OOPS"
-          : "OK" + (outcome == ProverInterface.Outcome.Invalid ? "" : " (" + outcome + ")"));
+          : "OK" + (outcome == SolverOutcome.Invalid ? "" : " (" + outcome + ")"));
     }
 
-    if (outcome == ProverInterface.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 460a2acdc..fdcf1e80f 100644
--- a/Source/VCGeneration/Split.cs
+++ b/Source/VCGeneration/Split.cs
@@ -9,6 +9,7 @@
 using Microsoft.BaseTypes;
 using Microsoft.Boogie.VCExprAST;
 using Microsoft.Boogie.SMTLib;
+using VCGeneration;
 
 namespace VC
 {
@@ -17,56 +18,21 @@ namespace VC
 
   public class Split : ProofRun
   {
-      private VCGenOptions options;
+      public VCGenOptions Options { get; }
 
-      public int? RandomSeed => Implementation.RandomSeed ?? options.RandomSeed;
-      private Random randomGen;
+      public int? RandomSeed => Implementation.RandomSeed ?? Options.RandomSeed;
+      private readonly Random randomGen;
 
-      private ImplementationRun run;
-
-      class BlockStats
-      {
-        public bool bigBlock;
-        public int id;
-        public double assertionCost;
-        public double assumptionCost; // before multiplier
-        public double incomingPaths;
-
-        public List<Block> /*!>!*/
-          virtualSuccessors = new List<Block>();
-
-        public List<Block> /*!>!*/
-          virtualPredecessors = new List<Block>();
-
-        public HashSet<Block> reachableBlocks;
-        public readonly Block block;
-
-        [ContractInvariantMethod]
-        void ObjectInvariant()
-        {
-          Contract.Invariant(cce.NonNullElements(virtualSuccessors));
-          Contract.Invariant(cce.NonNullElements(virtualPredecessors));
-          Contract.Invariant(block != null);
-        }
-
-
-        public BlockStats(Block b, int i)
-        {
-          Contract.Requires(b != null);
-          block = b;
-          assertionCost = -1;
-          id = i;
-        }
-      }
+      public ImplementationRun Run { get; }
 
       [ContractInvariantMethod]
       void ObjectInvariant()
       {
-        Contract.Invariant(cce.NonNullElements(blocks));
+        Contract.Invariant(cce.NonNullElements(Blocks));
         Contract.Invariant(cce.NonNullElements(bigBlocks));
         Contract.Invariant(cce.NonNullDictionaryAndValues(stats));
         Contract.Invariant(cce.NonNullElements(assumizedBranches));
-        Contract.Invariant(gotoCmdOrigins != null);
+        Contract.Invariant(GotoCmdOrigins != null);
         Contract.Invariant(parent != null);
         Contract.Invariant(Implementation != null);
         Contract.Invariant(copies != null);
@@ -75,8 +41,8 @@ void ObjectInvariant()
       }
 
 
-      private readonly List<Block> blocks;
-      public List<AssertCmd> Asserts => blocks.SelectMany(block => block.cmds.OfType<AssertCmd>()).ToList();
+      public List<Block> Blocks { get; }
+      public List<AssertCmd> Asserts => Blocks.SelectMany(block => block.cmds.OfType<AssertCmd>()).ToList();
       public readonly IReadOnlyList<Declaration> TopLevelDeclarations;
       readonly List<Block> bigBlocks = new();
 
@@ -96,13 +62,11 @@ void ObjectInvariant()
       int assertionCount;
       double assertionCost; // without multiplication by paths
 
-      Dictionary<TransferCmd, ReturnCmd> /*!*/
-        gotoCmdOrigins;
+      public Dictionary<TransferCmd, ReturnCmd> GotoCmdOrigins { get; }
 
-      readonly public VCGen /*!*/
-        parent;
+      public readonly VerificationConditionGenerator /*!*/ parent;
 
-      public Implementation /*!*/ Implementation => run.Implementation;
+      public Implementation /*!*/ Implementation => Run.Implementation;
 
       Dictionary<Block /*!*/, Block /*!*/> /*!*/
         copies = new Dictionary<Block /*!*/, Block /*!*/>();
@@ -120,20 +84,20 @@ readonly public VCGen /*!*/
 
       // 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);
         Contract.Requires(par != null);
-        this.blocks = blocks;
-        this.gotoCmdOrigins = gotoCmdOrigins;
+        this.Blocks = blocks;
+        this.GotoCmdOrigins = gotoCmdOrigins;
         this.parent = par;
-        this.run = run;
-        this.options = options;
+        this.Run = run;
+        this.Options = options;
         Interlocked.Increment(ref currentId);
 
         TopLevelDeclarations = par.program.TopLevelDeclarations;
@@ -145,14 +109,14 @@ public Split(VCGenOptions options, List<Block /*!*/> /*!*/ blocks,
 
       private void PrintTopLevelDeclarationsForPruning(Program program, Implementation implementation, string suffix)
       {
-        if (!options.Prune || options.PrintPrunedFile == null)
+        if (!Options.Prune || Options.PrintPrunedFile == null)
         {
           return;
         }
 
         using var writer = new TokenTextWriter(
-          $"{options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}.bpl", false,
-          options.PrettyPrint, options);
+          $"{Options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}.bpl", false,
+          Options.PrettyPrint, Options);
 
         var functionAxioms = 
           program.Functions.Where(f => f.DefinitionAxioms.Any()).SelectMany(f => f.DefinitionAxioms);
@@ -230,17 +194,17 @@ public void DumpDot(int splitNum)
         string filename = string.Format("{0}.split.{1}.bpl", Implementation.Name, splitNum);
         using (System.IO.StreamWriter sw = System.IO.File.CreateText(filename))
         {
-          int oldPrintUnstructured = options.PrintUnstructured;
-          options.PrintUnstructured = 2; // print only the unstructured program
-          bool oldPrintDesugaringSetting = options.PrintDesugarings;
-          options.PrintDesugarings = false;
+          int oldPrintUnstructured = Options.PrintUnstructured;
+          Options.PrintUnstructured = 2; // print only the unstructured program
+          bool oldPrintDesugaringSetting = Options.PrintDesugarings;
+          Options.PrintDesugarings = false;
           List<Block> backup = Implementation.Blocks;
           Contract.Assert(backup != null);
-          Implementation.Blocks = blocks;
-          Implementation.Emit(new TokenTextWriter(filename, sw, /*setTokens=*/ false, /*pretty=*/ false, options), 0);
+          Implementation.Blocks = Blocks;
+          Implementation.Emit(new TokenTextWriter(filename, sw, /*setTokens=*/ false, /*pretty=*/ false, Options), 0);
           Implementation.Blocks = backup;
-          options.PrintDesugarings = oldPrintDesugaringSetting;
-          options.PrintUnstructured = oldPrintUnstructured;
+          Options.PrintDesugarings = oldPrintDesugaringSetting;
+          Options.PrintUnstructured = oldPrintUnstructured;
         }
       }
 
@@ -357,13 +321,13 @@ void ComputeBestSplit()
 
         assertionCount = 0;
 
-        foreach (Block b in blocks)
+        foreach (Block b in Blocks)
         {
           Contract.Assert(b != null);
           CountAssertions(b);
         }
 
-        foreach (Block b in blocks)
+        foreach (Block b in Blocks)
         {
           Contract.Assert(b != null);
           BlockStats bs = GetBlockStats(b);
@@ -376,7 +340,7 @@ void ComputeBestSplit()
               BlockStats chs = GetBlockStats(ch);
               if (!chs.bigBlock)
               {
-                options.OutputWriter.WriteLine("non-big {0} accessed from {1}", ch, b);
+                Options.OutputWriter.WriteLine("non-big {0} accessed from {1}", ch, b);
                 DumpDot(-1);
                 Contract.Assert(false);
                 throw new cce.UnreachableException();
@@ -446,7 +410,7 @@ void ComputeBestSplit()
           }
         }
 
-        if (options.VcsPathSplitMult * score > totalCost)
+        if (Options.VcsPathSplitMult * score > totalCost)
         {
           splitBlock = null;
           score = -1;
@@ -485,7 +449,7 @@ void UpdateIncommingPaths(BlockStats s)
 
           if (count > 1)
           {
-            s.incomingPaths *= options.VcsPathJoinMult;
+            s.incomingPaths *= Options.VcsPathJoinMult;
           }
         }
       }
@@ -534,11 +498,11 @@ void ComputeBlockSets(bool allowSmall)
         keepAtAll.Clear();
 
         Debug.Assert(splitBlock == null || GetBlockStats(splitBlock).bigBlock);
-        Debug.Assert(GetBlockStats(blocks[0]).bigBlock);
+        Debug.Assert(GetBlockStats(Blocks[0]).bigBlock);
 
         if (assertToAssume)
         {
-          foreach (Block b in allowSmall ? blocks : bigBlocks)
+          foreach (Block b in allowSmall ? Blocks : bigBlocks)
           {
             Contract.Assert(b != null);
             if (ComputeReachableNodes(b).Contains(cce.NonNull(splitBlock)))
@@ -563,7 +527,7 @@ void ComputeBlockSets(bool allowSmall)
         }
         else
         {
-          ComputeBlockSetsHelper(blocks[0], allowSmall);
+          ComputeBlockSetsHelper(Blocks[0], allowSmall);
         }
       }
 
@@ -584,7 +548,7 @@ double DoComputeScore(bool aa)
           GetBlockStats(b).incomingPaths = -1.0;
         }
 
-        GetBlockStats(blocks[0]).incomingPaths = 1.0;
+        GetBlockStats(Blocks[0]).incomingPaths = 1.0;
 
         double cost = 0.0;
         foreach (Block b in bigBlocks)
@@ -597,14 +561,14 @@ double DoComputeScore(bool aa)
             double local = s.assertionCost;
             if (ShouldAssumize(b))
             {
-              local = (s.assertionCost + s.assumptionCost) * options.VcsAssumeMult;
+              local = (s.assertionCost + s.assumptionCost) * Options.VcsAssumeMult;
             }
             else
             {
-              local = s.assumptionCost * options.VcsAssumeMult + s.assertionCost;
+              local = s.assumptionCost * Options.VcsAssumeMult + s.assertionCost;
             }
 
-            local = local + local * s.incomingPaths * options.VcsPathCostMult;
+            local = local + local * s.incomingPaths * Options.VcsPathCostMult;
             cost += local;
           }
         }
@@ -652,7 +616,7 @@ List<Cmd> SliceCmds(Block b)
 
             if (swap)
             {
-              theNewCmd = VCGen.AssertTurnedIntoAssume(options, a);
+              theNewCmd = VerificationConditionGenerator.AssertTurnedIntoAssume(Options, a);
             }
           }
 
@@ -704,18 +668,18 @@ Split DoSplit()
         Contract.Ensures(Contract.Result<Split>() != null);
 
         copies.Clear();
-        CloneBlock(blocks[0]);
+        CloneBlock(Blocks[0]);
         List<Block> newBlocks = new List<Block>();
         Dictionary<TransferCmd, ReturnCmd> newGotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();
-        foreach (Block b in blocks)
+        foreach (Block b in Blocks)
         {
           Contract.Assert(b != null);
           if (copies.TryGetValue(b, out var tmp))
           {
             newBlocks.Add(cce.NonNull(tmp));
-            if (gotoCmdOrigins.ContainsKey(b.TransferCmd))
+            if (GotoCmdOrigins.ContainsKey(b.TransferCmd))
             {
-              newGotoCmdOrigins[tmp.TransferCmd] = gotoCmdOrigins[b.TransferCmd];
+              newGotoCmdOrigins[tmp.TransferCmd] = GotoCmdOrigins[b.TransferCmd];
             }
 
             foreach (Block p in b.Predecessors)
@@ -729,7 +693,7 @@ Split DoSplit()
           }
         }
 
-        return new Split(options, newBlocks, newGotoCmdOrigins, parent, run);
+        return new Split(Options, newBlocks, newGotoCmdOrigins, parent, Run);
       }
 
       Split SplitAt(int idx)
@@ -767,8 +731,8 @@ void Print()
       {
         List<Block> tmp = Implementation.Blocks;
         Contract.Assert(tmp != null);
-        Implementation.Blocks = blocks;
-        ConditionGeneration.EmitImpl(options, run, false);
+        Implementation.Blocks = Blocks;
+        ConditionGeneration.EmitImpl(Options, Run, false);
         Implementation.Blocks = tmp;
       }
 
@@ -778,13 +742,13 @@ public Counterexample ToCounterexample(ProverContext context)
         Contract.Ensures(Contract.Result<Counterexample>() != null);
 
         List<Block> trace = new List<Block>();
-        foreach (Block b in blocks)
+        foreach (Block b in Blocks)
         {
           Contract.Assert(b != null);
           trace.Add(b);
         }
 
-        foreach (Block b in blocks)
+        foreach (Block b in Blocks)
         {
           Contract.Assert(b != null);
           foreach (Cmd c in b.Cmds)
@@ -792,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;
             }
@@ -803,339 +767,12 @@ public Counterexample ToCounterexample(ProverContext context)
         throw new cce.UnreachableException();
       }
 
-      // Verify b with the last split in blockAssignments[b]
-      private static Dictionary<Block, Block> PickBlocksToVerify (List<Block> blocks, Dictionary<Block, int> splitPoints)
-      {
-        var todo = new Stack<Block>();
-        var blockAssignments = new Dictionary<Block, Block>();
-        var immediateDominator = (Program.GraphFromBlocks(blocks)).ImmediateDominator();
-        todo.Push(blocks[0]);
-        while(todo.Count > 0)
-        {
-          var currentBlock = todo.Pop();
-          if (blockAssignments.Keys.Contains(currentBlock))
-          {
-            continue;
-          }
-          else if (immediateDominator[currentBlock] == currentBlock) // if the currentBlock doesn't have a predecessor.
-          {
-            blockAssignments[currentBlock] = currentBlock;
-          }
-          else if (splitPoints.Keys.Contains(immediateDominator[currentBlock])) // if the currentBlock's dominator has a split then it will be associated with that split
-          {
-            blockAssignments[currentBlock] = immediateDominator[currentBlock];
-          }
-          else
-          {
-            Contract.Assert(blockAssignments.Keys.Contains(immediateDominator[currentBlock]));
-            blockAssignments[currentBlock] = blockAssignments[immediateDominator[currentBlock]];
-          }
-          if (currentBlock.TransferCmd is GotoCmd exit)
-          {
-            exit.labelTargets.ForEach(blk => todo.Push(blk));
-          }
-        }
-        return blockAssignments;
-      }
-      private static List<Block> DoPreAssignedManualSplit(VCGenOptions options, List<Block> blocks, Dictionary<Block, Block> blockAssignments, int splitNumberWithinBlock,
-        Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert)
-      {
-        var newBlocks = new List<Block>(blocks.Count()); // Copies of the original blocks
-        var duplicator = new Duplicator();
-        var oldToNewBlockMap = new Dictionary<Block, Block>(blocks.Count()); // Maps original blocks to their new copies in newBlocks
-        foreach (var currentBlock in blocks)
-        {
-          var newBlock = (Block)duplicator.VisitBlock(currentBlock);
-          oldToNewBlockMap[currentBlock] = newBlock;
-          newBlocks.Add(newBlock);
-          if (currentBlock == containingBlock)
-          {
-            var newCmds = new List<Cmd>();
-            var splitCount = -1;
-            var verify = splitCount == splitNumberWithinBlock;
-            foreach (Cmd c in currentBlock.Cmds)
-            {
-              if (ShouldSplitHere(c, splitOnEveryAssert))
-              {
-                splitCount++;
-                verify = splitCount == splitNumberWithinBlock;
-              }
-              newCmds.Add(verify ? c : AssertIntoAssume(options, c));
-            }
-            newBlock.Cmds = newCmds;
-          }
-          else if (lastSplitInBlock && blockAssignments[currentBlock] == containingBlock)
-          {
-            var verify = true;
-            var newCmds = new List<Cmd>();
-            foreach(Cmd c in currentBlock.Cmds) {
-              verify = !ShouldSplitHere(c, splitOnEveryAssert) && verify;
-              newCmds.Add(verify ? c : AssertIntoAssume(options, c));
-            }
-            newBlock.Cmds = newCmds;
-          }
-          else
-          {
-            newBlock.Cmds = currentBlock.Cmds.Select<Cmd, Cmd>(x => AssertIntoAssume(options, x)).ToList();
-          }
-        }
-        // Patch the edges between the new blocks
-        foreach (var oldBlock in blocks)
-        {
-          if (oldBlock.TransferCmd is ReturnCmd)
-          {
-            continue;
-          }
-
-          var gotoCmd = (GotoCmd)oldBlock.TransferCmd;
-          var newLabelTargets = new List<Block>(gotoCmd.labelTargets.Count());
-          var newLabelNames = new List<string>(gotoCmd.labelTargets.Count());
-          foreach (var target in gotoCmd.labelTargets)
-          {
-            newLabelTargets.Add(oldToNewBlockMap[target]);
-            newLabelNames.Add(oldToNewBlockMap[target].Label);
-          }
-
-          oldToNewBlockMap[oldBlock].TransferCmd = new GotoCmd(gotoCmd.tok, newLabelNames, newLabelTargets);
-        }
-        return newBlocks;
-      }
-
-      private static List<Block> PostProcess(List<Block> blocks)
-      {
-        void DeleteFalseGotos (Block b)
-        {
-          bool isAssumeFalse (Cmd c) { return c is AssumeCmd ac && ac.Expr is LiteralExpr le && !le.asBool; }
-          var firstFalseIdx = b.Cmds.FindIndex(c => isAssumeFalse(c));
-          if (firstFalseIdx != -1)
-          {
-            b.Cmds = b.Cmds.Take(firstFalseIdx + 1).ToList();
-            b.TransferCmd = (b.TransferCmd is GotoCmd) ? new ReturnCmd(b.tok) : b.TransferCmd;
-          }
-        }
-
-        bool ContainsAssert(Block b)
-        {
-          bool isNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); }
-          return b.Cmds.Exists(cmd => isNonTrivialAssert(cmd));
-        }
-
-        blocks.ForEach(b => DeleteFalseGotos(b)); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously
-        var todo = new Stack<Block>();
-        var peeked = new HashSet<Block>();
-        var interestingBlocks = new HashSet<Block>();
-        todo.Push(blocks[0]);
-        while(todo.Count() > 0)
-        {
-          var currentBlock = todo.Peek();
-          var pop = peeked.Contains(currentBlock);
-          peeked.Add(currentBlock);
-          var interesting = false;
-          var exit = currentBlock.TransferCmd as GotoCmd;
-          if (exit != null && !pop) {
-            exit.labelTargets.ForEach(b => todo.Push(b));
-          } else if (exit != null) {
-            Contract.Assert(pop);
-            var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList());
-            currentBlock.TransferCmd = gtc;
-            interesting = interesting || gtc.labelTargets.Count() != 0;
-          }
-          if (pop)
-          {
-            interesting = interesting || ContainsAssert(currentBlock);
-            if (interesting) {
-              interestingBlocks.Add(currentBlock);
-            }
-            todo.Pop();
-          }
-        }
-        interestingBlocks.Add(blocks[0]); // must not be empty
-        return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders.
-      }
-
-      private static bool ShouldSplitHere(Cmd c, bool splitOnEveryAssert) {
-        return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "split_here")
-               || c is AssertCmd && splitOnEveryAssert;
-      }
-      
-      public static List<Split /*!*/> FindManualSplits(Split initialSplit, bool splitOnEveryAssert)
-      {
-        Contract.Requires(initialSplit.Implementation != null);
-        Contract.Ensures(Contract.Result<List<Split>>() == null || cce.NonNullElements(Contract.Result<List<Split>>()));
-
-        var splitPoints = new Dictionary<Block, int>();
-        foreach (var b in initialSplit.blocks)
-        {
-          foreach (Cmd c in b.Cmds)
-          {
-            var p = c as PredicateCmd;
-            if (ShouldSplitHere(c, splitOnEveryAssert))
-            {
-              splitPoints.TryGetValue(b, out var count);
-              splitPoints[b] = count + 1;
-            }
-          }
-        }
-        var splits = new List<Split>();
-        if (!splitPoints.Any())
-        {
-          splits.Add(initialSplit);
-        }
-        else
-        {
-          Block entryPoint = initialSplit.blocks[0];
-          var blockAssignments = PickBlocksToVerify(initialSplit.blocks, splitPoints);
-          var entryBlockHasSplit = splitPoints.Keys.Contains(entryPoint);
-          var baseSplitBlocks = PostProcess(DoPreAssignedManualSplit(initialSplit.options, initialSplit.blocks, blockAssignments, -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert));
-          splits.Add(new Split(initialSplit.options, baseSplitBlocks, initialSplit.gotoCmdOrigins, initialSplit.parent, initialSplit.run));
-          foreach (KeyValuePair<Block, int> pair in splitPoints)
-          {
-            for (int i = 0; i < pair.Value; i++)
-            {
-              bool lastSplitInBlock = i == pair.Value - 1;
-              var newBlocks = DoPreAssignedManualSplit(initialSplit.options, initialSplit.blocks, blockAssignments, i, pair.Key, lastSplitInBlock, splitOnEveryAssert);
-              splits.Add(new Split(initialSplit.options, PostProcess(newBlocks), initialSplit.gotoCmdOrigins, initialSplit.parent, initialSplit.run)); // REVIEW: Does gotoCmdOrigins need to be changed at all?
-            }
-          }
-        }
-        return splits;
-      }
-
-      public static List<Split> FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VCGen par)
-      {
-        bool IsFocusCmd(Cmd c) {
-          return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus");
-        }
-
-        List<Block> GetFocusBlocks(List<Block> blocks) {
-          return blocks.Where(blk => blk.Cmds.Any(c => IsFocusCmd(c))).ToList();
-        }
-
-        var impl = run.Implementation;
-        var dag = Program.GraphFromImpl(impl);
-        var topoSorted = dag.TopologicalSort().ToList();
-        // By default, we process the foci in a top-down fashion, i.e., in the topological order.
-        // If the user sets the RelaxFocus flag, we use the reverse (topological) order.
-        var focusBlocks = GetFocusBlocks(topoSorted);
-        if (par.CheckerPool.Options.RelaxFocus) {
-          focusBlocks.Reverse();
-        }
-        if (!focusBlocks.Any()) {
-          var f = new List<Split>();
-          f.Add(new Split(options, impl.Blocks, gotoCmdOrigins, par, run));
-          return f;
-        }
-        // finds all the blocks dominated by focusBlock in the subgraph
-        // which only contains vertices of subgraph.
-        HashSet<Block> DominatedBlocks(Block focusBlock, IEnumerable<Block> subgraph)
-        {
-          var dominators = new Dictionary<Block, HashSet<Block>>();
-          var todo = new Queue<Block>();
-          foreach (var b in topoSorted.Where(blk => subgraph.Contains(blk)))
-          {
-            var s = new HashSet<Block>();
-            var pred = b.Predecessors.Where(blk => subgraph.Contains(blk)).ToList();
-            if (pred.Count != 0)
-            {
-              s.UnionWith(dominators[pred[0]]);
-              pred.ForEach(blk => s.IntersectWith(dominators[blk]));
-            }
-            s.Add(b);
-            dominators[b] = s;
-          }
-          return subgraph.Where(blk => dominators[blk].Contains(focusBlock)).ToHashSet();
-        }
-
-        Cmd DisableSplits(Cmd c)
-        {
-          if (c is PredicateCmd pc)
-          {
-            for (var kv = pc.Attributes; kv != null; kv = kv.Next)
-            {
-              if (kv.Key == "split")
-              {
-                kv.AddParam(new LiteralExpr(Token.NoToken, false));
-              }
-            }
-          }
-          return c;
-        }
-
-        var Ancestors = new Dictionary<Block, HashSet<Block>>();
-        var Descendants = new Dictionary<Block, HashSet<Block>>();
-        focusBlocks.ForEach(fb => Ancestors[fb] = dag.ComputeReachability(fb, false).ToHashSet());
-        focusBlocks.ForEach(fb => Descendants[fb] = dag.ComputeReachability(fb, true).ToHashSet());
-        var s = new List<Split>();
-        var duplicator = new Duplicator();
-        void FocusRec(int focusIdx, IEnumerable<Block> blocks, IEnumerable<Block> freeBlocks)
-        {
-          if (focusIdx == focusBlocks.Count())
-          {
-            // it is important for l to be consistent with reverse topological order.
-            var l = dag.TopologicalSort().Where(blk => blocks.Contains(blk)).Reverse();
-            // assert that the root block, impl.Blocks[0], is in l
-            Contract.Assert(l.ElementAt(l.Count() - 1) == impl.Blocks[0]);
-            var newBlocks = new List<Block>();
-            var oldToNewBlockMap = new Dictionary<Block, Block>(blocks.Count());
-            foreach (Block b in l)
-            {
-              var newBlock = (Block)duplicator.Visit(b);
-              newBlocks.Add(newBlock);
-              oldToNewBlockMap[b] = newBlock;
-              // freeBlocks consist of the predecessors of the relevant foci.
-              // Their assertions turn into assumes and any splits inside them are disabled.
-              if(freeBlocks.Contains(b))
-              {
-                newBlock.Cmds = b.Cmds.Select(c => Split.AssertIntoAssume(options, c)).Select(c => DisableSplits(c)).ToList();
-              }
-              if (b.TransferCmd is GotoCmd gtc)
-              {
-                var targets = gtc.labelTargets.Where(blk => blocks.Contains(blk));
-                newBlock.TransferCmd = new GotoCmd(gtc.tok,
-                                              targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(),
-                                              targets.Select(blk => oldToNewBlockMap[blk]).ToList());
-              }
-            }
-            newBlocks.Reverse();
-            Contract.Assert(newBlocks[0] == oldToNewBlockMap[impl.Blocks[0]]);
-            s.Add(new Split(options, PostProcess(newBlocks), gotoCmdOrigins, par, run));
-          }
-          else if (!blocks.Contains(focusBlocks[focusIdx])
-                    || freeBlocks.Contains(focusBlocks[focusIdx]))
-          {
-            FocusRec(focusIdx + 1, blocks, freeBlocks);
-          }
-          else
-          {
-            var b = focusBlocks[focusIdx]; // assert b in blocks
-            var dominatedBlocks = DominatedBlocks(b, blocks);
-            // the first part takes all blocks except the ones dominated by the focus block
-            FocusRec(focusIdx + 1, blocks.Where(blk => !dominatedBlocks.Contains(blk)), freeBlocks);
-            var ancestors = Ancestors[b];
-            ancestors.Remove(b);
-            var descendants = Descendants[b];
-            // the other part takes all the ancestors, the focus block, and the descendants.
-            FocusRec(focusIdx + 1, ancestors.Union(descendants).Intersect(blocks), ancestors.Union(freeBlocks));
-          }
-        }
-
-        FocusRec(0, impl.Blocks, new List<Block>());
-        return s;
-      }
-
-      public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VCGen par, bool splitOnEveryAssert)
-      {
-        List<Split> focussedImpl = FocusImpl(options, run, gotoCmdOrigins, par);
-        var splits = focussedImpl.Select(s => FindManualSplits(s, splitOnEveryAssert)).SelectMany(x => x).ToList();
-        return splits;
-      }
-
       public static List<Split /*!*/> /*!*/ DoSplit(Split initial, double splitThreshold, int maxSplits)
       {
         Contract.Requires(initial != null);
         Contract.Ensures(cce.NonNullElements(Contract.Result<List<Split>>()));
 
-        var run = initial.run;
+        var run = initial.Run;
         var result = new List<Split> { initial };
 
         while (result.Count < maxSplits)
@@ -1161,7 +798,7 @@ public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun
 
           Split s0, s1;
 
-          bool splitStats = initial.options.TraceVerify;
+          bool splitStats = initial.Options.TraceVerify;
 
           if (splitStats)
           {
@@ -1208,12 +845,12 @@ public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun
           {
             var ss = new List<Block>
             {
-              s0.blocks[0],
-              s1.blocks[0]
+              s0.Blocks[0],
+              s1.Blocks[0]
             };
             try
             {
-              best.SoundnessCheck(new HashSet<List<Block>>(new BlockListComparer()), best.blocks[0], ss);
+              best.SoundnessCheck(new HashSet<List<Block>>(new BlockListComparer()), best.Blocks[0], ss);
             }
             catch (System.Exception e)
             {
@@ -1234,7 +871,7 @@ public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun
             run.OutputWriter.WriteLine("    --> {0}", s1.Stats);
           }
 
-          if (initial.options.TraceVerify)
+          if (initial.Options.TraceVerify)
           {
             best.Print();
           }
@@ -1246,60 +883,37 @@ public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun
         return result;
       }
 
-      class BlockListComparer : IEqualityComparer<List<Block>>
-      {
-        public bool Equals(List<Block> x, List<Block> y)
-        {
-          return x == y || x.SequenceEqual(y);
-        }
-
-        public int GetHashCode(List<Block> obj)
-        {
-          int h = 0;
-          Contract.Assume(obj != null);
-          foreach (var b in obj)
-          {
-            if (b != null)
-            {
-              h += b.GetHashCode();
-            }
-          }
-
-          return h;
-        }
-      }
-
-      public (ProverInterface.Outcome outcome, VCResult 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);
-        ProverInterface.Outcome outcome = cce.NonNull(checker).ReadOutcome();
+        Bpl.SolverOutcome outcome = cce.NonNull(checker).ReadOutcome();
 
-        if (options.Trace && SplitIndex >= 0)
+        if (Options.Trace && SplitIndex >= 0)
         {
-          run.OutputWriter.WriteLine("      --> split #{0} done,  [{1} s] {2}", SplitIndex + 1,
+          Run.OutputWriter.WriteLine("      --> split #{0} done,  [{1} s] {2}", SplitIndex + 1,
             checker.ProverRunTime.TotalSeconds, outcome);
         }
-        if (options.Trace && options.TrackVerificationCoverage) {
-          run.OutputWriter.WriteLine("Proof dependencies:\n  {0}",
+        if (Options.Trace && Options.TrackVerificationCoverage) {
+          Run.OutputWriter.WriteLine("Proof dependencies:\n  {0}",
             string.Join("\n  ", CoveredElements.Select(s => s.Description).OrderBy(s => s)));
         }
 
         var resourceCount = checker.GetProverResourceCount();
-        var result = new VCResult(
-          vcNum: SplitIndex + 1,
-          iteration: iteration,
-          startTime: checker.ProverStart,
-          outcome: outcome,
-          runTime: checker.ProverRunTime,
-          maxCounterExamples: checker.Options.ErrorLimit,
-          counterExamples: Counterexamples,
-          asserts: Asserts,
-          coveredElements: CoveredElements,
-          resourceCount: resourceCount,
-          solverUsed: (options as SMTLibSolverOptions)?.Solver);
+        var result = new VerificationRunResult(
+          VcNum: SplitIndex + 1,
+          Iteration: iteration,
+          StartTime: checker.ProverStart,
+          Outcome: outcome,
+          RunTime: checker.ProverRunTime,
+          MaxCounterExamples: checker.Options.ErrorLimit,
+          CounterExamples: Counterexamples,
+          Asserts: Asserts,
+          CoveredElements: CoveredElements,
+          ResourceCount: resourceCount,
+          SolverUsed: (Options as SMTLibSolverOptions)?.Solver);
         callback.OnVCResult(result);
 
-        if (options.VcsDumpSplits)
+        if (Options.VcsDumpSplits)
         {
           DumpDot(SplitIndex);
         }
@@ -1323,13 +937,13 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa
         VCExpr vc;
         // Lock impl since we're setting impl.Blocks that is used to generate the VC.
         lock (Implementation) {
-          Implementation.Blocks = blocks;
+          Implementation.Blocks = Blocks;
 
           var absyIds = new ControlFlowIdMap<Absy>();
 
           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;
@@ -1343,13 +957,13 @@ 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);
         }
 
-        if (options.TraceVerify && SplitIndex >= 0)
+        if (Options.TraceVerify && SplitIndex >= 0)
         {
-          run.OutputWriter.WriteLine("-- after split #{0}", SplitIndex);
+          Run.OutputWriter.WriteLine("-- after split #{0}", SplitIndex);
           Print();
         }
 
@@ -1370,16 +984,6 @@ public string Description
         }
       }
 
-      private static Cmd AssertIntoAssume(VCGenOptions options, Cmd c)
-      {
-        if (c is AssertCmd assrt)
-        {
-          return VCGen.AssertTurnedIntoAssume(options, assrt);
-        }
-
-        return c;
-      }
-
       private void SoundnessCheck(HashSet<List<Block> /*!*/> /*!*/ cache, Block /*!*/ orig,
         List<Block /*!*/> /*!*/ copies)
       {
diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs
index e2e1336a0..7409ca17e 100644
--- a/Source/VCGeneration/SplitAndVerifyWorker.cs
+++ b/Source/VCGeneration/SplitAndVerifyWorker.cs
@@ -7,14 +7,15 @@
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Boogie;
+using VCGeneration;
 using static VC.ConditionGeneration;
 
 namespace VC
 {
   class SplitAndVerifyWorker
   {
-    public IObservable<(Split split, VCResult vcResult)> BatchCompletions => batchCompletions;
-    private readonly Subject<(Split split, VCResult vcResult)> batchCompletions = new();
+    public IObservable<(Split split, VerificationRunResult vcResult)> BatchCompletions => batchCompletions;
+    private readonly Subject<(Split split, VerificationRunResult vcResult)> batchCompletions = new();
 
     private readonly VCGenOptions options;
     private readonly VerifierCallback callback;
@@ -30,8 +31,8 @@ class SplitAndVerifyWorker
     private bool TrackingProgress => DoSplitting && (callback.OnProgress != null || options.Trace); 
     private bool KeepGoing => maxKeepGoingSplits > 1;
 
-    private VCGen vcGen;
-    private Outcome outcome;
+    private VerificationConditionGenerator verificationConditionGenerator;
+    private VcOutcome vcOutcome;
     private double remainingCost;
     private double provenCost;
     private int total;
@@ -39,25 +40,25 @@ 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,
-      Outcome outcome)
+      VcOutcome vcOutcome)
     {
       this.options = options;
       this.callback = callback;
       this.mvInfo = mvInfo;
       this.run = run;
-      this.outcome = outcome;
-      this.vcGen = vcGen;
+      this.vcOutcome = vcOutcome;
+      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;
@@ -67,7 +68,7 @@ public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun
       Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert);
 
       ResetPredecessors(Implementation.Blocks);
-      manualSplits = Split.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);
@@ -77,7 +78,7 @@ public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun
       splitNumber = DoSplitting ? 0 : -1;
     }
 
-    public async Task<Outcome> WorkUntilDone(CancellationToken cancellationToken)
+    public async Task<VcOutcome> WorkUntilDone(CancellationToken cancellationToken)
     {
       TrackSplitsCost(manualSplits);
       try
@@ -89,7 +90,7 @@ public async Task<Outcome> WorkUntilDone(CancellationToken cancellationToken)
         batchCompletions.OnCompleted();
       }
 
-      return outcome;
+      return vcOutcome;
     }
 
     public int ResourceCount => totalResourceCount;
@@ -168,7 +169,7 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch
 
       var (newOutcome, result, newResourceCount) = split.ReadOutcome(iteration, checker, callback);
       lock (this) {
-        outcome = MergeOutcomes(outcome, newOutcome);
+        vcOutcome = MergeOutcomes(vcOutcome, newOutcome);
         totalResourceCount += newResourceCount;
       }
       var proverFailed = IsProverFailed(newOutcome);
@@ -195,17 +196,17 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch
       }
     }
 
-    private static bool IsProverFailed(ProverInterface.Outcome outcome)
+    private static bool IsProverFailed(SolverOutcome outcome)
     {
       switch (outcome)
       {
-        case ProverInterface.Outcome.Valid:
-        case ProverInterface.Outcome.Invalid:
-        case ProverInterface.Outcome.Undetermined:
+        case SolverOutcome.Valid:
+        case SolverOutcome.Invalid:
+        case SolverOutcome.Undetermined:
           return false;
-        case ProverInterface.Outcome.OutOfMemory:
-        case ProverInterface.Outcome.TimeOut:
-        case ProverInterface.Outcome.OutOfResource:
+        case SolverOutcome.OutOfMemory:
+        case SolverOutcome.TimeOut:
+        case SolverOutcome.OutOfResource:
           return true;
         default:
           Contract.Assert(false);
@@ -213,48 +214,48 @@ private static bool IsProverFailed(ProverInterface.Outcome outcome)
       }
     }
 
-    private static Outcome MergeOutcomes(Outcome currentOutcome, ProverInterface.Outcome newOutcome)
+    private static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, SolverOutcome newOutcome)
     {
       switch (newOutcome)
       {
-        case ProverInterface.Outcome.Valid:
-          return currentOutcome;
-        case ProverInterface.Outcome.Invalid:
-          return Outcome.Errors;
-        case ProverInterface.Outcome.OutOfMemory:
-          if (currentOutcome != Outcome.Errors && currentOutcome != Outcome.Inconclusive)
+        case SolverOutcome.Valid:
+          return currentVcOutcome;
+        case SolverOutcome.Invalid:
+          return VcOutcome.Errors;
+        case SolverOutcome.OutOfMemory:
+          if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive)
           {
-            return Outcome.OutOfMemory;
+            return VcOutcome.OutOfMemory;
           }
 
-          return currentOutcome;
-        case ProverInterface.Outcome.TimeOut:
-          if (currentOutcome != Outcome.Errors && currentOutcome != Outcome.Inconclusive)
+          return currentVcOutcome;
+        case SolverOutcome.TimeOut:
+          if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive)
           {
-            return Outcome.TimedOut;
+            return VcOutcome.TimedOut;
           }
 
-          return currentOutcome;
-        case ProverInterface.Outcome.OutOfResource:
-          if (currentOutcome != Outcome.Errors && currentOutcome != Outcome.Inconclusive)
+          return currentVcOutcome;
+        case SolverOutcome.OutOfResource:
+          if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive)
           {
-            return Outcome.OutOfResource;
+            return VcOutcome.OutOfResource;
           }
 
-          return currentOutcome;
-        case ProverInterface.Outcome.Undetermined:
-          if (currentOutcome != Outcome.Errors)
+          return currentVcOutcome;
+        case SolverOutcome.Undetermined:
+          if (currentVcOutcome != VcOutcome.Errors)
           {
-            return Outcome.Inconclusive;
+            return VcOutcome.Inconclusive;
           }
-          return currentOutcome;
+          return currentVcOutcome;
         default:
           Contract.Assert(false);
           throw new cce.UnreachableException();
       }
     }
 
-    private async Task HandleProverFailure(Split split, Checker checker, VerifierCallback callback, VCResult vcResult, CancellationToken cancellationToken)
+    private async Task HandleProverFailure(Split split, Checker checker, VerifierCallback callback, VerificationRunResult verificationRunResult, CancellationToken cancellationToken)
     {
       if (split.LastChance) {
         string msg = "some timeout";
@@ -266,11 +267,11 @@ private async Task HandleProverFailure(Split split, Checker checker, VerifierCal
         callback.OnCounterexample(cex, msg);
         split.Counterexamples.Add(cex);
         // Update one last time the result with the dummy counter-example to indicate the position of the timeout
-        var result = vcResult with {
-          counterExamples = split.Counterexamples
+        var result = verificationRunResult with {
+          CounterExamples = split.Counterexamples
         };
         batchCompletions.OnNext((split, result));
-        outcome = Outcome.Errors;
+        vcOutcome = VcOutcome.Errors;
         await checker.GoBackToIdle();
         return;
       }
@@ -286,29 +287,29 @@ private async Task HandleProverFailure(Split split, Checker checker, VerifierCal
         maxVcCost = 1.0; // for future
         TrackSplitsCost(newSplits);
         
-        if (outcome != Outcome.Errors) {
-          outcome = Outcome.Correct;
+        if (vcOutcome != VcOutcome.Errors) {
+          vcOutcome = VcOutcome.Correct;
         }
         await Task.WhenAll(newSplits.Select(newSplit => DoWorkForMultipleIterations(newSplit, cancellationToken)));
         return;
       }
 
-      Contract.Assert(outcome != Outcome.Correct);
-      if (outcome == Outcome.TimedOut) {
+      Contract.Assert(vcOutcome != VcOutcome.Correct);
+      if (vcOutcome == VcOutcome.TimedOut) {
         string msg = "some timeout";
         if (split.reporter is { resourceExceededMessage: { } }) {
           msg = split.reporter.resourceExceededMessage;
         }
 
         callback.OnTimeout(msg);
-      } else if (outcome == Outcome.OutOfMemory) {
+      } else if (vcOutcome == VcOutcome.OutOfMemory) {
         string msg = "out of memory";
         if (split.reporter is { resourceExceededMessage: { } }) {
           msg = split.reporter.resourceExceededMessage;
         }
 
         callback.OnOutOfMemory(msg);
-      } else if (outcome == Outcome.OutOfResource) {
+      } else if (vcOutcome == VcOutcome.OutOfResource) {
         string msg = "out of resource";
         if (split.reporter is { resourceExceededMessage: { } }) {
           msg = split.reporter.resourceExceededMessage;
@@ -317,7 +318,7 @@ private async Task HandleProverFailure(Split split, Checker checker, VerifierCal
         callback.OnOutOfResource(msg);
       }
 
-      batchCompletions.OnNext((split, vcResult));
+      batchCompletions.OnNext((split, verificationRunResult));
     }
   }
 }
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index bb48650f4..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)
     {
@@ -990,7 +990,7 @@ protected override bool ProcIsLoop(string procname)
       return true;
     }
 
-    public abstract Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars);
+    public abstract VcOutcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars);
   }
 
 } // namespace VC
diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VerificationConditionGenerator.cs
similarity index 98%
rename from Source/VCGeneration/VCGen.cs
rename to Source/VCGeneration/VerificationConditionGenerator.cs
index ed3393daa..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;
@@ -355,8 +355,8 @@ record ImplementationTransformationData {
 
     private static ConditionalWeakTable<Implementation, ImplementationTransformationData> implementationData = new();
 
-    public override async Task<Outcome> VerifyImplementation(ImplementationRun run, VerifierCallback callback,
-      CancellationToken cancellationToken, IObserver<(Split split, VCResult vcResult)> batchCompletedObserver)
+    public override async Task<VcOutcome> VerifyImplementation(ImplementationRun run, VerifierCallback callback,
+      CancellationToken cancellationToken, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver)
     {
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
 
@@ -364,7 +364,7 @@ public override async Task<Outcome> VerifyImplementation(ImplementationRun run,
 
       if (run.Implementation.IsSkipVerification(Options))
       {
-        return Outcome.Inconclusive; // not sure about this one
+        return VcOutcome.Inconclusive; // not sure about this one
       }
 
       callback.OnProgress?.Invoke("VCgen", 0, 0, 0.0);
@@ -391,12 +391,12 @@ public override async Task<Outcome> VerifyImplementation(ImplementationRun run,
         ExpandAsserts(impl);
       }
 
-      Outcome outcome = Outcome.Correct;
+      VcOutcome vcOutcome = VcOutcome.Correct;
 
       // Report all recycled failing assertions for this implementation.
       if (impl.RecycledFailingAssertions != null && impl.RecycledFailingAssertions.Any())
       {
-        outcome = Outcome.Errors;
+        vcOutcome = VcOutcome.Errors;
         foreach (var a in impl.RecycledFailingAssertions)
         {
           var checksum = a.Checksum;
@@ -417,21 +417,21 @@ public override async Task<Outcome> VerifyImplementation(ImplementationRun run,
       }
 
       var worker = new SplitAndVerifyWorker(Options, this, run, data.GotoCmdOrigins, callback,
-        data.ModelViewInfo, outcome);
+        data.ModelViewInfo, vcOutcome);
       worker.BatchCompletions.Subscribe(batchCompletedObserver);
             
-      outcome = await worker.WorkUntilDone(cancellationToken);
+      vcOutcome = await worker.WorkUntilDone(cancellationToken);
       ResourceCount = worker.ResourceCount;
 
       TotalProverElapsedTime = worker.TotalProverElapsedTime;
-      if (outcome == Outcome.Correct && smokeTester != null)
+      if (vcOutcome == VcOutcome.Correct && smokeTester != null)
       {
         await smokeTester.Test(run.OutputWriter);
       }
 
       callback.OnProgress?.Invoke("done", 0, 0, 1.0);
 
-      return outcome;
+      return vcOutcome;
     }
 
     public class ErrorReporter : ProverInterface.ErrorHandler {
@@ -501,7 +501,7 @@ public ErrorReporter(VCGenOptions options,
       }
 
       public override void OnModel(IList<string> labels /*!*/ /*!*/, Model model,
-        ProverInterface.Outcome proverOutcome)
+        Bpl.SolverOutcome proverOutcome)
       {
         // no counter examples reported.
         if (labels.Count == 0)
diff --git a/Source/VCGeneration/VerificationResultCollector.cs b/Source/VCGeneration/VerificationResultCollector.cs
new file mode 100644
index 000000000..6957914ad
--- /dev/null
+++ b/Source/VCGeneration/VerificationResultCollector.cs
@@ -0,0 +1,45 @@
+using System.Collections.Concurrent;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
+
+namespace VC;
+
+public class VerificationResultCollector : VerifierCallback
+{
+  private readonly VCGenOptions options;
+
+  public VerificationResultCollector(VCGenOptions options) : base(options.PrintProverWarnings)
+  {
+    this.options = options;
+  }
+
+  [ContractInvariantMethod]
+  void ObjectInvariant()
+  {
+    Contract.Invariant(cce.NonNullElements(examples));
+    Contract.Invariant(cce.NonNullElements(vcResults));
+  }
+
+  public readonly ConcurrentQueue<Counterexample> examples = new();
+  public readonly ConcurrentQueue<VerificationRunResult> vcResults = new();
+
+  public override void OnCounterexample(Counterexample ce, string /*?*/ reason)
+  {
+    //Contract.Requires(ce != null);
+    ce.InitializeModelStates();
+    examples.Enqueue(ce);
+  }
+
+  public override void OnUnreachableCode(ImplementationRun run)
+  {
+    //Contract.Requires(impl != null);
+    run.OutputWriter.WriteLine("found unreachable code:");
+    ConditionGeneration.EmitImpl(options, run, false);
+    // TODO report error about next to last in seq
+  }
+
+  public override void OnVCResult(VerificationRunResult result)
+  {
+    vcResults.Enqueue(result);
+  }
+}
\ No newline at end of file
diff --git a/Source/VCGeneration/VCResult.cs b/Source/VCGeneration/VerificationRunResult.cs
similarity index 62%
rename from Source/VCGeneration/VCResult.cs
rename to Source/VCGeneration/VerificationRunResult.cs
index a304b1158..5704dca80 100644
--- a/Source/VCGeneration/VCResult.cs
+++ b/Source/VCGeneration/VerificationRunResult.cs
@@ -15,28 +15,28 @@ namespace VC
   using Bpl = Microsoft.Boogie;
   using System.Threading.Tasks;
 
-  public record VCResult
+  public record VerificationRunResult
   (
-    int vcNum,
-    int iteration,
-    DateTime startTime,
-    ProverInterface.Outcome outcome,
-    TimeSpan runTime,
-    int maxCounterExamples,
-    List<Counterexample> counterExamples,
-    List<AssertCmd> asserts,
-    IEnumerable<TrackedNodeComponent> coveredElements,
-    int resourceCount,
-    SolverKind? solverUsed
+    int VcNum,
+    int Iteration,
+    DateTime StartTime,
+    Bpl.SolverOutcome Outcome,
+    TimeSpan RunTime,
+    int MaxCounterExamples,
+    List<Counterexample> CounterExamples,
+    List<AssertCmd> Asserts,
+    IEnumerable<TrackedNodeComponent> CoveredElements,
+    int ResourceCount,
+    SolverKind? SolverUsed
   ) {
-    public void ComputePerAssertOutcomes(out Dictionary<AssertCmd, ProverInterface.Outcome> perAssertOutcome,
+    public void ComputePerAssertOutcomes(out Dictionary<AssertCmd, Bpl.SolverOutcome> perAssertOutcome,
       out Dictionary<AssertCmd, Counterexample> perAssertCounterExamples) {
       perAssertOutcome = new();
       perAssertCounterExamples = new();
-      if (outcome == ProverInterface.Outcome.Valid) {
-        perAssertOutcome = asserts.ToDictionary(cmd => cmd, assertCmd => ProverInterface.Outcome.Valid);
+      if (Outcome == Bpl.SolverOutcome.Valid) {
+        perAssertOutcome = Asserts.ToDictionary(cmd => cmd, assertCmd => Bpl.SolverOutcome.Valid);
       } else {
-        foreach (var counterExample in counterExamples) {
+        foreach (var counterExample in CounterExamples) {
           AssertCmd underlyingAssert;
           if (counterExample is AssertCounterexample assertCounterexample) {
             underlyingAssert = assertCounterexample.FailingAssert;
@@ -49,25 +49,25 @@ public void ComputePerAssertOutcomes(out Dictionary<AssertCmd, ProverInterface.O
           }
 
           // We ensure that the underlyingAssert is among the original asserts
-          if (!asserts.Contains(underlyingAssert)) {
+          if (!Asserts.Contains(underlyingAssert)) {
             continue;
           }
 
-          perAssertOutcome.TryAdd(underlyingAssert, ProverInterface.Outcome.Invalid);
+          perAssertOutcome.TryAdd(underlyingAssert, Bpl.SolverOutcome.Invalid);
           perAssertCounterExamples.TryAdd(underlyingAssert, counterExample);
         }
 
         var remainingOutcome =
-          outcome == ProverInterface.Outcome.Invalid && counterExamples.Count < maxCounterExamples
+          Outcome == Bpl.SolverOutcome.Invalid && CounterExamples.Count < MaxCounterExamples
             // We could not extract more counterexamples, remaining assertions are thus valid 
-            ? ProverInterface.Outcome.Valid
-            : outcome == ProverInterface.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
-              ? ProverInterface.Outcome.Undetermined
+              ? Bpl.SolverOutcome.Undetermined
               // TimeOut, OutOfMemory, OutOfResource, Undetermined for a single split also applies to assertions
-              : outcome;
+              : Outcome;
 
-        foreach (var assert in asserts) {
+        foreach (var assert in Asserts) {
           perAssertOutcome.TryAdd(assert, remainingOutcome);
         }
       }
diff --git a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl
index 4d04b75ff..29f5c5ba7 100644
--- a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl
+++ b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl
@@ -5,31 +5,36 @@ const n:int;
 axiom n >= 1;
 
 type val = int;
-type {:linear "collect", "broadcast"} pid = int;
+type pid = int;
+
+datatype {:linear "perm"} perm {
+  Broadcast(i: int),
+  Collect(i: int)
+}
 
 function {:inline} pid(i:int) : bool { 1 <= i && i <= n }
 
 function {:inline} InitialBroadcastPAs (k:pid) : [BROADCAST]bool
 {
-  (lambda pa:BROADCAST :: pid(pa->i) && pa->i < k)
+  (lambda pa:BROADCAST :: pa->p == Broadcast(pa->i) && pid(pa->i) && pa->i < k)
 }
 
 function {:inline} InitialCollectPAs (k:pid) : [COLLECT]bool
 {
-  (lambda pa:COLLECT :: pid(pa->i) && pa->i < k)
+  (lambda pa:COLLECT :: pa->p == Collect(pa->i) && pid(pa->i) && pa->i < k)
 }
 
 function {:inline} AllBroadcasts () : [BROADCAST]bool
-{ (lambda pa:BROADCAST :: pid(pa->i)) }
+{ (lambda pa:BROADCAST :: pa->p == Broadcast(pa->i) && pid(pa->i)) }
 
 function {:inline} AllCollects () : [COLLECT]bool
-{ (lambda pa:COLLECT :: pid(pa->i)) }
+{ (lambda pa:COLLECT :: pa->p == Collect(pa->i) && pid(pa->i)) }
 
 function {:inline} RemainingBroadcasts (k:pid) : [BROADCAST]bool
-{ (lambda {:pool "Broadcast"} pa:BROADCAST :: k < pa->i && pa->i <= n) }
+{ (lambda {:pool "Broadcast"} pa:BROADCAST :: pa->p == Broadcast(pa->i) && k < pa->i && pa->i <= n) }
 
 function {:inline} RemainingCollects (k:pid) : [COLLECT]bool
-{ (lambda {:pool "Collect"} pa:COLLECT :: k < pa->i && pa->i <= n) }
+{ (lambda {:pool "Collect"} pa:COLLECT :: pa->p == Collect(pa->i) && k < pa->i && pa->i <= n) }
 
 ////////////////////////////////////////////////////////////////////////////////
 
@@ -61,16 +66,11 @@ function value_card(v:val, value:[pid]val, i:pid, j:pid) : int
 
 ////////////////////////////////////////////////////////////////////////////////
 
-// NOTE: Civl currently does not support variables to be linear in multiple
-// domains (i.e., supplying multiple linear annotations). In the future we
-// would like the MAIN action(s) to take a single parameter as follows:
-//     {:linear_in "broadcast"}{:linear_in "collect"} pids:[pid]bool
-
 atomic action {:layer 4}
-MAIN''({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool)
+MAIN''({:linear_in "perm"} ps:[perm]bool)
 modifies CH, decision;
 {
-  assert pidsBroadcast == (lambda i:pid :: pid(i)) && pidsCollect == pidsBroadcast;
+  assert ps == (lambda p:perm :: pid(p->i));
   assert CH == MultisetEmpty;
   CH := (lambda v:val :: value_card(v, value, 1, n));
   assume card(CH) == n;
@@ -79,13 +79,13 @@ modifies CH, decision;
 }
 
 action {:layer 3}
-INV_COLLECT_ELIM({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool)
+INV_COLLECT_ELIM({:linear_in "perm"} ps:[perm]bool)
 creates COLLECT;
 modifies CH, decision;
 {
   var {:pool "INV_COLLECT"} k: int;
 
-  assert pidsBroadcast == (lambda i:pid :: pid(i)) && pidsCollect == pidsBroadcast;
+  assert ps == (lambda p:perm :: pid(p->i));
   assert CH == MultisetEmpty;
 
   CH := (lambda v:val :: value_card(v, value, 1, n));
@@ -94,23 +94,23 @@ modifies CH, decision;
 
   assume
     {:add_to_pool "INV_COLLECT", k, k+1}
-    {:add_to_pool "Collect", COLLECT(n)}
+    {:add_to_pool "Collect", COLLECT(Collect(n), n)}
     0 <= k && k <= n;
   decision := (lambda i:pid :: if 1 <= i && i <= k then max(CH) else decision[i]);
   call create_asyncs(RemainingCollects(k));
-  call set_choice(COLLECT(k+1));
+  call set_choice(COLLECT(Collect(k+1), k+1));
 }
 
 ////////////////////////////////////////////////////////////////////////////////
 
 atomic action {:layer 3}
-MAIN'({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool)
+MAIN'({:linear_in "perm"} ps:[perm]bool)
 refines MAIN'' using INV_COLLECT_ELIM;
 creates COLLECT;
 eliminates COLLECT using COLLECT';
 modifies CH;
 {
-  assert pidsBroadcast == (lambda i:pid :: pid(i)) && pidsCollect == pidsBroadcast;
+  assert ps == (lambda p:perm :: pid(p->i));
   assert CH == MultisetEmpty;
 
   assume {:add_to_pool "INV_COLLECT", 0} true;
@@ -121,11 +121,11 @@ modifies CH;
 }
 
 atomic action {:layer 2}
-MAIN({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool)
+MAIN({:linear_in "perm"} ps:[perm]bool)
 refines MAIN' using INV_BROADCAST_ELIM;
 creates BROADCAST, COLLECT;
 {
-  assert pidsBroadcast == (lambda i:pid :: pid(i)) && pidsCollect == pidsBroadcast;
+  assert ps == (lambda p:perm :: pid(p->i));
 
   assume {:add_to_pool "INV_BROADCAST", 0} true;
   assert CH == MultisetEmpty;
@@ -135,52 +135,52 @@ creates BROADCAST, COLLECT;
 }
 
 action {:layer 2}
-INV_BROADCAST_ELIM({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool)
+INV_BROADCAST_ELIM({:linear_in "perm"} ps:[perm]bool)
 creates BROADCAST, COLLECT;
 modifies CH;
 {
   var {:pool "INV_BROADCAST"} k: int;
 
-  assert pidsBroadcast == (lambda i:pid :: pid(i)) && pidsCollect == pidsBroadcast;
+  assert ps == (lambda p:perm :: pid(p->i));
   assert CH == MultisetEmpty;
 
   assume
     {:add_to_pool "INV_BROADCAST", k, k+1}
-    {:add_to_pool "Broadcast", BROADCAST(n)}
+    {:add_to_pool "Broadcast", BROADCAST(Broadcast(n), n)}
     0 <= k && k <= n;
   CH := (lambda v:val :: value_card(v, value, 1, k));
   assume card(CH) == k;
   assume MultisetSubsetEq(MultisetEmpty, CH);
   call create_asyncs(RemainingBroadcasts(k));
   call create_asyncs(AllCollects());
-  call set_choice(BROADCAST(k+1));
+  call set_choice(BROADCAST(Broadcast(k+1), k+1));
 }
 
-async left action {:layer 2} BROADCAST({:linear_in "broadcast"} i:pid)
+async left action {:layer 2} BROADCAST({:linear_in "perm"} p:perm, i:pid)
 modifies CH;
 {
-  assert pid(i);
+  assert pid(i) && p == Broadcast(i);
   CH := CH[value[i] := CH[value[i]] + 1];
 }
 
-async atomic action {:layer 2,3} COLLECT({:linear_in "collect"} i:pid)
+async atomic action {:layer 2,3} COLLECT({:linear_in "perm"} p:perm, i:pid)
 modifies decision;
 {
   var received_values:[val]int;
-  assert pid(i);
+  assert pid(i) && p == Collect(i);
   assume card(received_values) == n;
   assume MultisetSubsetEq(MultisetEmpty, received_values);
   assume MultisetSubsetEq(received_values, CH);
   decision[i] := max(received_values);
 }
 
-action {:layer 3} COLLECT'({:linear_in "collect"} i:pid)
+action {:layer 3} COLLECT'({:linear_in "perm"} p:perm, i:pid)
 modifies decision;
 {
   assert CH == (lambda v:val :: value_card(v, value, 1, n));
   assert card(CH) == n;
   assert MultisetSubsetEq(MultisetEmpty, CH);
-  call COLLECT(i);
+  call COLLECT(p, i);
 }
 
 ////////////////////////////////////////////////////////////////////////////////
@@ -201,45 +201,43 @@ pure procedure {:inline 1} add_to_multiset (CH:[val]int, x: val) returns (CH':[v
 ////////////////////////////////////////////////////////////////////////////////
 
 yield invariant {:layer 1}
-YieldInit({:linear "broadcast"} pidsBroadcast:[pid]bool, {:linear "collect"} pidsCollect:[pid]bool);
-invariant pidsBroadcast == (lambda ii:pid :: pid(ii)) && pidsCollect == pidsBroadcast;
+YieldInit({:linear "perm"} ps:[perm]bool);
+invariant ps == (lambda p:perm :: pid(p->i));
 invariant (forall ii:pid :: CH_low[ii] == MultisetEmpty);
 invariant CH == MultisetEmpty;
 
 yield procedure {:layer 1}
-Main({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool)
+Main({:linear_in "perm"} ps:[perm]bool)
 refines MAIN;
-requires call YieldInit(pidsBroadcast, pidsCollect);
+requires call YieldInit(ps);
 {
   var {:pending_async}{:layer 1} Broadcast_PAs:[BROADCAST]int;
   var {:pending_async}{:layer 1} Collect_PAs:[COLLECT]int;
   var i:pid;
-  var {:linear "broadcast"} s:pid;
-  var {:linear "collect"} r:pid;
-  var {:linear "broadcast"} ss:[pid]bool;
-  var {:linear "collect"} rr:[pid]bool;
+  var {:linear "perm"} s:perm;
+  var {:linear "perm"} r:perm;
+  var {:linear "perm"} ps':[perm]bool;
 
-  ss := pidsBroadcast;
-  rr := pidsCollect;
+  ps' := ps;
   i := 1;
   while (i <= n)
   invariant {:layer 1} 1 <= i && i <= n + 1;
-  invariant {:layer 1} ss == (lambda ii:pid :: pid(ii) && ii >= i) && ss == rr;
+  invariant {:layer 1} ps' == (lambda p:perm :: pid(p->i) && p->i >= i);
   invariant {:layer 1} Broadcast_PAs == ToMultiset(InitialBroadcastPAs(i));
   invariant {:layer 1} Collect_PAs == ToMultiset(InitialCollectPAs(i));
   {
-    call s, r, ss, rr := linear_transfer(i, ss, rr);
-    async call Broadcast(s);
-    async call Collect(r);
+    call s, r, ps' := linear_transfer(i, ps');
+    async call Broadcast(s, i);
+    async call Collect(r, i);
     i := i + 1;
   }
   assert {:layer 1} Broadcast_PAs == ToMultiset(AllBroadcasts());
   assert {:layer 1} Collect_PAs == ToMultiset(AllCollects());
 }
 
-yield procedure {:layer 1} Broadcast({:linear_in "broadcast"} i:pid)
+yield procedure {:layer 1} Broadcast({:linear_in "perm"} p:perm, i:pid)
 refines BROADCAST;
-requires {:layer 1} pid(i);
+requires {:layer 1} pid(i) && p == Broadcast(i);
 {
   var j: pid;
   var v: val;
@@ -250,7 +248,7 @@ requires {:layer 1} pid(i);
   j := 1;
   while (j <= n)
   invariant {:layer 1} 1 <= j && j <= n+1;
-  invariant {:layer 1} CH_low == (lambda jj: pid :: (if pid(jj) && jj < j then MultisetPlus(old_CH_low[jj], MultisetSingleton(value[i])) else old_CH_low[jj]));
+  invariant {:layer 1} CH_low == (lambda jj: pid :: (if pid(jj) && jj < j then MultisetPlus(old_CH_low[jj], MultisetSingleton(value[p->i])) else old_CH_low[jj]));
   {
     call send(v, j);
     j := j + 1;
@@ -259,10 +257,10 @@ requires {:layer 1} pid(i);
 }
 
 yield procedure {:layer 1}
-Collect({:linear_in "collect"} i:pid)
+Collect({:linear_in "perm"} p:perm, i:pid)
 refines COLLECT;
 requires call YieldInv();
-requires {:layer 1} pid(i);
+requires {:layer 1} pid(i) && p == Collect(i);
 {
   var j: pid;
   var d: val;
@@ -287,7 +285,7 @@ requires {:layer 1} pid(i);
     received_values[v] := received_values[v] + 1;
     j := j + 1;
   }
-  call set_decision(i, d);
+  call set_decision(p, d);
 }
 
 ////////////////////////////////////////////////////////////////////////////////
@@ -297,10 +295,11 @@ both action {:layer 1} GET_VALUE(i:pid) returns (v:val)
   v := value[i];
 }
 
-both action {:layer 1} SET_DECISION({:linear_in "collect"} i:pid, d:val)
+both action {:layer 1} SET_DECISION({:linear_in "perm"} p:perm, d:val)
 modifies decision;
 {
-  decision[i] := d;
+  assert p is Collect;
+  decision[p->i] := d;
 }
 
 left action {:layer 1} SEND(v:val, i:pid)
@@ -317,18 +316,18 @@ modifies CH_low;
 }
 
 both action {:layer 1}
-LINEAR_TRANSFER(i:pid, {:linear_in "broadcast"} ss:[pid]bool, {:linear_in "collect"} rr:[pid]bool)
-returns ({:linear "broadcast"} s:pid, {:linear "collect"} r:pid, {:linear "broadcast"} ss':[pid]bool, {:linear "collect"} rr':[pid]bool)
+LINEAR_TRANSFER(i:pid, {:linear_in "perm"} ps:[perm]bool)
+returns ({:linear "perm"} s:perm, {:linear "perm"} r:perm, {:linear "perm"} ps':[perm]bool)
 {
-  assert ss[i] && rr[i];
-  s, r := i, i;
-  ss', rr' := ss[i := false], rr[i := false];
+  assert ps[Broadcast(i)] && ps[Collect(i)];
+  s, r := Broadcast(i), Collect(i);
+  ps' := ps[s := false][r := false];
 }
 
 yield procedure {:layer 0} get_value(i:pid) returns (v:val);
 refines GET_VALUE;
 
-yield procedure {:layer 0} set_decision({:linear_in "collect"} i:pid, d:val);
+yield procedure {:layer 0} set_decision({:linear_in "perm"} p:perm, d:val);
 refines SET_DECISION;
 
 yield procedure {:layer 0} send(v:val, i:pid);
@@ -337,8 +336,8 @@ refines SEND;
 yield procedure {:layer 0} receive(i:pid) returns (v:val);
 refines RECEIVE;
 
-yield procedure {:layer 0} linear_transfer(i:pid, {:linear_in "broadcast"} ss:[pid]bool, {:linear_in "collect"} rr:[pid]bool)
-returns ({:linear "broadcast"} s:pid, {:linear "collect"} r:pid, {:linear "broadcast"} ss':[pid]bool, {:linear "collect"} rr':[pid]bool);
+yield procedure {:layer 0} linear_transfer(i:pid, {:linear_in "perm"} ps:[perm]bool)
+returns ({:linear "perm"} s:perm, {:linear "perm"} r:perm, {:linear "perm"} ps':[perm]bool);
 refines LINEAR_TRANSFER;
 
 ////////////////////////////////////////////////////////////////////////////////
diff --git a/Test/civl/regression-tests/linear/typecheck.bpl b/Test/civl/regression-tests/linear/typecheck.bpl
index e0b728223..9092d00c8 100644
--- a/Test/civl/regression-tests/linear/typecheck.bpl
+++ b/Test/civl/regression-tests/linear/typecheck.bpl
@@ -2,24 +2,24 @@
 // RUN: %diff "%s.expect" "%t"
 
 type X;
-type {:linear "A", "B", "C", "D", "D2", "x", "", "lin"} Lin = int;
+type {:linear "D"} Lin = int;
 
 procedure A()
 {
-    var {:linear "A"} a: X;
-    var {:linear "A"} b: int;
+    var {:linear "D"} a: X;
+    var {:linear "D"} b: int;
 }
 
 procedure B()
 {
-    var {:linear "B"} a: X;
-    var {:linear "B"} b: [X]bool;
+    var {:linear "D"} a: X;
+    var {:linear "D"} b: [X]bool;
 }
 
 procedure C()
 {
-    var {:linear "C"} a: X;
-    var {:linear "C"} c: [X]int;
+    var {:linear "D"} a: X;
+    var {:linear "D"} c: [X]int;
 }
 
 function f(X): X;
@@ -30,7 +30,7 @@ yield procedure {:layer 1} D()
     var {:linear "D"} x: X;
     var {:linear "D"} b: [X]bool;
     var c: X;
-    var {:linear "D2"} d: X;
+    var {:linear "D"} d: X;
 
     b[a] := true;
 
@@ -68,20 +68,20 @@ yield procedure {:layer 1} E({:linear_in "D"} a: X, {:linear_in "D"} b: X) retur
 
 yield procedure {:layer 1} F({:linear_in "D"} a: X) returns ({:linear "D"} c: X);
 
-var {:linear "x"} g:int;
+var {:linear "D"} g:int;
 
-procedure G(i:int) returns({:linear "x"} r:int)
+procedure G(i:int) returns({:linear "D"} r:int)
 {
   r := g;
 }
 
-procedure H(i:int) returns({:linear "x"} r:int)
+procedure H(i:int) returns({:linear "D"} r:int)
 modifies g;
 {
   g := r;
 }
 
-yield procedure {:layer 1} I({:linear_in ""} x:int) returns({:linear ""} x':int)
+yield procedure {:layer 1} I({:linear_in "D"} x:int) returns({:linear "D"} x':int)
 {
   x' := x;
 }
@@ -90,13 +90,13 @@ yield procedure {:layer 1} J()
 {
 }
 
-yield procedure {:layer 1} P1({:linear_in ""} x:int) returns({:linear ""} x':int)
+yield procedure {:layer 1} P1({:linear_in "D"} x:int) returns({:linear "D"} x':int)
 {
   par x' := I(x) | J();
   call x' := I(x');
 }
 
-yield procedure {:layer 1} P2({:linear_in ""} x:int) returns({:linear ""} x':int)
+yield procedure {:layer 1} P2({:linear_in "D"} x:int) returns({:linear "D"} x':int)
 {
   call x' := I(x);
   par x' := I(x') | J();
diff --git a/Test/civl/regression-tests/linear/typecheck.bpl.expect b/Test/civl/regression-tests/linear/typecheck.bpl.expect
index 15a7a7784..50ffc5805 100644
--- a/Test/civl/regression-tests/linear/typecheck.bpl.expect
+++ b/Test/civl/regression-tests/linear/typecheck.bpl.expect
@@ -1,14 +1,11 @@
 typecheck.bpl(35,9): Error: Only simple assignment allowed on linear variable b
 typecheck.bpl(37,6): Error: Only linear variable can be assigned to linear variable a
-typecheck.bpl(41,6): Error: The domains of source and target of assignment must be the same
 typecheck.bpl(47,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment
 typecheck.bpl(51,4): Error: Linear variable a can occur only once as an input parameter
 typecheck.bpl(53,4): Error: Only variable can be passed to linear parameter: f(a)
-typecheck.bpl(55,4): Error: The domains of parameter b and argument d must be the same
-typecheck.bpl(57,4): Error: The domains of formal and actual parameters must be the same
 typecheck.bpl(59,4): Error: Only linear variable can be passed to linear parameter: c
 typecheck.bpl(67,0): Error: Output variable d must be available at a return
 typecheck.bpl(76,0): Error: Global variable g must be available at a return
 typecheck.bpl(81,7): Error: unavailable source for a linear read
 typecheck.bpl(82,0): Error: Output variable r must be available at a return
-13 type checking errors detected in typecheck.bpl
+10 type checking errors detected in typecheck.bpl
diff --git a/Test/civl/regression-tests/perm2.bpl b/Test/civl/regression-tests/perm2.bpl
deleted file mode 100644
index 22ba8fae9..000000000
--- a/Test/civl/regression-tests/perm2.bpl
+++ /dev/null
@@ -1,100 +0,0 @@
-// RUN: %parallel-boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-type {:linear "tid", "1", "2"} IntTid = int;
-
-var {:layer 0,1} g: int;
-var {:layer 0,1} h: int;
-var {:layer 0,1}{:linear "tid"} unallocated:[int]bool;
-
-atomic action {:layer 1} AtomicSetG(val:int)
-modifies g;
-{g := val; }
-
-yield procedure {:layer 0} SetG(val:int);
-refines AtomicSetG;
-
-atomic action {:layer 1} AtomicSetH(val:int)
-modifies h;
-{ h := val; }
-
-yield procedure {:layer 0} SetH(val:int);
-refines AtomicSetH;
-
-yield procedure {:layer 1} Allocate() returns ({:linear "tid"} xl: int)
-ensures {:layer 1} xl != 0;
-{
-    call xl := AllocateLow();
-}
-
-atomic action {:layer 1} AtomicAllocateLow() returns ({:linear "tid"} xls: int)
-modifies unallocated;
-{ assume xls != 0; assume unallocated[xls]; unallocated[xls] := false; }
-
-yield procedure {:layer 0} AllocateLow() returns ({:linear "tid"} xls: int);
-refines AtomicAllocateLow;
-
-yield procedure {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int)
-requires {:layer 1} x == MapConst(true);
-requires {:layer 1} y == MapConst(true);
-{
-    var {:linear "tid"} tid_child: int;
-    tid_out := tid_in;
-
-    call SetG(0);
-
-    call Yield_g(x);
-
-    call tid_child := Allocate();
-    async call B(tid_child, x);
-
-    call Yield();
-
-    call SetH(0);
-
-    call Yield_h(y);
-
-    call tid_child := Allocate();
-    async call C(tid_child, y);
-
-}
-
-yield procedure {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool)
-requires {:layer 1} x_in != MapConst(false);
-{
-    var {:linear "tid"} tid_out: int;
-    var {:linear "1"} x: [int]bool;
-    tid_out := tid_in;
-    x := x_in;
-
-    call SetG(1);
-
-    call Yield();
-
-    call SetG(2);
-}
-
-yield procedure {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool)
-requires {:layer 1} y_in != MapConst(false);
-{
-    var {:linear "tid"} tid_out: int;
-    var {:linear "2"} y: [int]bool;
-    tid_out := tid_in;
-    y := y_in;
-
-    call SetH(1);
-
-    call Yield();
-
-    call SetH(2);
-}
-
-yield invariant {:layer 1} Yield_g({:linear "1"} x: [int]bool);
-invariant x == MapConst(true);
-invariant g == 0;
-
-yield invariant {:layer 1} Yield_h({:linear "2"} y: [int]bool);
-invariant y == MapConst(true);
-invariant h == 0;
-
-yield invariant {:layer 1} Yield();
diff --git a/Test/civl/regression-tests/perm2.bpl.expect b/Test/civl/regression-tests/perm2.bpl.expect
deleted file mode 100644
index 3e6d423af..000000000
--- a/Test/civl/regression-tests/perm2.bpl.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/civl/regression-tests/perm4.bpl b/Test/civl/regression-tests/perm4.bpl
deleted file mode 100644
index 79b479afa..000000000
--- a/Test/civl/regression-tests/perm4.bpl
+++ /dev/null
@@ -1,91 +0,0 @@
-// RUN: %parallel-boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-type {:linear "tid", "1", "2"} X = int;
-var {:layer 0,1} g: int;
-var {:layer 0,1} h: int;
-
-var {:layer 0,1}{:linear "tid"} unallocated:[int]bool;
-
-atomic action {:layer 1} AtomicSetG(val:int)
-modifies g;
-{ g := val; }
-
-yield procedure {:layer 0} SetG(val:int);
-refines AtomicSetG;
-
-atomic action {:layer 1} AtomicSetH(val:int)
-modifies h;
-{ h := val; }
-
-yield procedure {:layer 0} SetH(val:int);
-refines AtomicSetH;
-
-yield invariant {:layer 1} Yield({:linear "1"} x: [int]bool);
-invariant x == MapConst(true) && g == 0;
-
-yield procedure {:layer 1} Allocate() returns ({:linear "tid"} xl: int)
-ensures {:layer 1} xl != 0;
-{
-    call xl := AllocateLow();
-}
-
-atomic action {:layer 1} AtomicAllocateLow() returns ({:linear "tid"} xls: int)
-modifies unallocated;
-{ assume xls != 0 && unallocated[xls]; unallocated[xls] := false; }
-
-yield procedure {:layer 0} AllocateLow() returns ({:linear "tid"} xls: int);
-refines AtomicAllocateLow;
-
-yield procedure {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int)
-requires {:layer 1} x == MapConst(true);
-requires {:layer 1} y == MapConst(true);
-{
-    var {:linear "tid"} tid_child: int;
-    tid_out := tid_in;
-
-    call SetG(0);
-
-    par tid_child := Allocate() | Yield(x);
-
-    async call B(tid_child, x);
-
-    call Yield_g(x);
-
-    call SetH(0);
-
-    call Yield_h(y);
-
-    call tid_child := Allocate();
-    async call C(tid_child, y);
-}
-
-yield procedure {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool)
-requires {:layer 1} x_in != MapConst(false);
-{
-    var {:linear "tid"} tid_out: int;
-    var {:linear "1"} x: [int]bool;
-    tid_out := tid_in;
-    x := x_in;
-
-    call SetG(1);
-}
-
-yield procedure {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool)
-requires {:layer 1} y_in != MapConst(false);
-{
-    var {:linear "tid"} tid_out: int;
-    var {:linear "2"} y: [int]bool;
-    tid_out := tid_in;
-    y := y_in;
-
-    call SetH(1);
-}
-
-yield invariant {:layer 1} Yield_g(x: [int]bool);
-invariant x == MapConst(true);
-invariant g == 0;
-
-yield invariant {:layer 1} Yield_h({:linear "2"} y: [int]bool);
-invariant y == MapConst(true);
-invariant h == 0;
diff --git a/Test/civl/regression-tests/perm4.bpl.expect b/Test/civl/regression-tests/perm4.bpl.expect
deleted file mode 100644
index 1b9cf6ab2..000000000
--- a/Test/civl/regression-tests/perm4.bpl.expect
+++ /dev/null
@@ -1,6 +0,0 @@
-perm4.bpl(87,1): Error: Non-interference check failed
-Execution trace:
-    perm4.bpl(68,13): anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_Yield_g$0$L
-
-Boogie program verifier finished with 4 verified, 1 error
diff --git a/Test/civl/samples/StoreBuffer.bpl b/Test/civl/samples/StoreBuffer.bpl
index 813759604..8e53467cc 100644
--- a/Test/civl/samples/StoreBuffer.bpl
+++ b/Test/civl/samples/StoreBuffer.bpl
@@ -1,6 +1,6 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-type {:linear "tid", "addr"} X = int;
+type {:linear "tid"} X = int;
 
 const numMutators: int;
 axiom 0 < numMutators;