More fixes

[andrii-a8c]

Fix three unrelated prover-side failure modes in split/parallel veriication

This addresses three independent bugs that surface under sui-prover's -vcsSplitOnEveryAssert + -vcsMaxKeepGoingSplits + -vcsCores>1 configuration on large, heavily-inlined Move specs (e.g. cetus clmm_math::*):

1. BlockRewriter.ComputeNewBlocks: rebuild Predecessors after DeleteBlocksNotLeadingToAssertions + BlockCoalescer.CoalesceInPlace (Source/VCGeneration/Splits/BlockRewriter.cs).

   ShallowClone leaves Predecessors empty, and both transformations rewrite gotos without touching the downstream Predecessors lists -- so the returned newBlocks reach Split.CountAssertions with empty predecessor lists. CountAssertions then reads next.Predecessors.Count as 0 for a block N that actually has multiple real predecessors, incorrectly merges N (setting N.bigBlock = false), and later finds another big block Q still referencing N in its virtualSuccessors. That trips the invariant at Split.cs:354 with "non-big N accessed from Q" and a Cce.UnreachableException that kills the whole verification.

   Mirrors the predecessor rebuild BlockTransformations.Optimize already performs after the same two steps.

2. SMTLibProcess.Send: make each SMT command atomic with respect to concurrent writers (Source/Provers/SMTLib/SMTLibProcess.cs).

   The asyncLock (SemaphoreSlim) only serializes the high-level async operations (SendRequest / PingPong / SendRequestsAndCloseInput); a large number of call sites invoke Send directly (SendThisVC during VC setup, Reset, RunTimeoutDiagnostics) without holding it. With -vcsCores>1 + keep-going splits, these paths can race against another checker's in-flight ping, and because StreamWriter.WriteLine may chunk the string and Flush is a separate call, bytes from two commands interleave on Z3's stdin. Z3 then reports diagnostics like

   unknown constant $IsValid'$<hash-truncated>(get-info :name)\n<hash-rest>
   

   -- the ping request literally spliced into the middle of a declare-fun identifier, followed by a cascade of unknown-constant, invalid-let-declaration, invalid-pop, and ControlFlow-already-declared errors as Z3 loses sync.

   Add a writerLock that guards the WriteLine + Flush pair so each command reaches Z3 as a single contiguous byte stream.

3. Pipe-death normalization across Send + ExecutionEngine (Source/Provers/SMTLib/SMTLibProcess.cs, Source/ExecutionEngine/ExecutionEngine.cs).

   When the solver process exits mid-verification (crash, OOM, hard timeout kill), Send's WriteLine/Flush throw ObjectDisposedException or IOException raw. Checker.Check's generic catch (Exception e) wraps them as UnexpectedProverOutputException(e.ToString()), and ExecutionEngine reports

   Advisory: <spec> SKIPPED because of internal error:
       unexpected prover output: System.ObjectDisposedException: ...
   

   with VcOutcome.Inconclusive.

   Convert those into the existing ProverDiedException in Send (already thrown from PingPong when Z3 returns null, so both code paths now speak the same language), and in ExecutionEngine.VerifyImplementationWithLargeThread replace the catch (ProverDiedException) { throw; } -- which today bubbles to VerifyEachImplementation and aborts the whole multi-spec run with "Fatal Error: ProverException" -- with a per-spec handler that emits a clean advisory and sets VcOutcome.SolverException, matching the sibling IOException branch.

Also: add .foxy/sessions to .gitignore.

Tested:

• dotnet build Source/Boogie.sln -c Release: 0 warnings, 0 errors (-warnaserror).
• dotnet test Source/Boogie.sln: 281/281 pass (CoreTests 58, ExecutionEngineTests 27, BaseTypesTests 196).
• lit Test/: 635 pass, 2 XFAIL; 6 remaining failures are pre-existing and environmental (cvc5 binary missing, Z3-version-specific model output). Verified they fail identically with these changes reverted.
• End-to-end on cetus_clmm_specs: clmm_math::get_delta_down_from_output_spec and clmm_math::get_liquidity_by_amount_spec now verify cleanly where they previously crashed with Cce.UnreachableException and ObjectDisposedException respectively.

[andreistefanescu]

👍