More fixes

.gitignore

@@ -42,3 +42,4 @@ Source/*.userprefs
 
 # Rider files
 .idea/
+.foxy/sessions

Source/ExecutionEngine/ExecutionEngine.cs

@@ -1020,9 +1020,17 @@ private Task<ImplementationRunResult> VerifyImplementationWithLargeThread(Proces
           verificationResult.Errors = null;
           verificationResult.VcOutcome = VcOutcome.Inconclusive;
         }
-        catch (ProverDiedException)
+        catch (ProverDiedException e)
         {
-          throw;
+          // Z3 (or whichever SMT solver) exited mid-verification -- crash, OOM,
+          // hard timeout kill, a malformed earlier command, etc. Surface it as a
+          // per-spec solver exception instead of propagating (which would abort
+          // the entire multi-spec run at VerifyEachImplementation).
+          Options.Printer.AdvisoryWriteLine(traceWriter,
+            "Advisory: {0} SKIPPED because the prover died: {1}",
+            impl.VerboseName, e.Message);
+          verificationResult.Errors = null;
+          verificationResult.VcOutcome = VcOutcome.SolverException;
         }
         catch (UnexpectedProverOutputException upo)
         {

Source/Provers/SMTLib/SMTLibProcess.cs

@@ -18,6 +18,16 @@ public class SMTLibProcess : SMTLibSolver {
     private readonly AsyncQueue<string> solverOutput = new();
     // Used to synchronise between requests into this class.
     private readonly SemaphoreSlim asyncLock = new(1);
+    // Guards the underlying stdin pipe so that a whole SMT command (WriteLine + Flush)
+    // is written atomically. asyncLock only serializes the high-level async operations
+    // (SendRequest / PingPong / SendRequestsAndCloseInput); plenty of call sites invoke
+    // Send directly while some *other* thread is holding asyncLock (e.g. a sync
+    // SendThisVC during VC setup concurrent with a ping from another checker under
+    // -vcsCores>1 + keep-going splits). Without this monitor the writer's chunked
+    // WriteLine + separate Flush can interleave, splicing one command's bytes into
+    // another -- which Z3 reports as "(get-info :name)" appearing inside a
+    // declare-fun identifier, "invalid let declaration", etc.
+    private readonly object writerLock = new();
     private TextWriter toProver;
     private readonly int smtProcessId;
     private static int smtProcessIdSeq = 0;
@@ -133,8 +143,36 @@ public override void Send(string cmd)
         Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);
       }
 
-      toProver.WriteLine(cmd);
-      toProver.Flush();
+      // If the solver process has already exited (crash, OOM, killed on timeout,
+      // etc.), its stdin pipe is closed; WriteLine/Flush throw ObjectDisposedException
+      // or IOException. Normalize those into ProverDiedException so upstream handlers
+      // can surface a clean per-spec SolverException instead of a noisy
+      // "unexpected prover output" advisory with a System.ObjectDisposedException
+      // stack trace as the message.
+      var writer = toProver;
+      if (writer == null)
+      {
+        throw new ProverDiedException();
+      }
+
+      // Hold writerLock across BOTH the WriteLine and the Flush so a single SMT
+      // command is written to Z3's stdin as a single contiguous byte stream.
+      try
+      {
+        lock (writerLock)
+        {
+          writer.WriteLine(cmd);
+          writer.Flush();
+        }
+      }
+      catch (ObjectDisposedException)
+      {
+        throw new ProverDiedException();
+      }
+      catch (IOException)
+      {
+        throw new ProverDiedException();
+      }
     }
 
     public override async Task<SExpr> SendRequest(string request, CancellationToken cancellationToken = default) {

Source/VCGeneration/Splits/BlockRewriter.cs

@@ -169,8 +169,18 @@ public List<Block> ComputeNewBlocks(
     newBlocks.Reverse();
 
     BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks);
-    
+
     BlockCoalescer.CoalesceInPlace(newBlocks);
+
+    // ShallowClone leaves Predecessors empty, and DeleteBlocksNotLeadingToAssertions
+    // / BlockCoalescer.CoalesceInPlace rewrite gotos without updating downstream
+    // Predecessors lists. Rebuild them so callers (notably Split.CountAssertions,
+    // which uses Predecessors.Count to decide block coalescing) see the final CFG.
+    foreach (var block in newBlocks) {
+      block.Predecessors.Clear();
+    }
+    Implementation.ComputePredecessorsForBlocks(newBlocks);
+
     return newBlocks;
   }