fixed crash issues

Source/Provers/SMTLib/NoopSolver.cs

@@ -39,7 +39,7 @@ public override void Send(string cmd)
 
   public override Task<SExpr> SendRequest(string request, CancellationToken cancellationToken = default) {
     Send(request);
-    return GetProverResponse();
+    return GetProverResponse(cancellationToken);
   }
 
   public override async Task<IReadOnlyList<SExpr>> SendRequestsAndCloseInput(IReadOnlyList<string> requests, CancellationToken cancellationToken = default) {
@@ -49,13 +49,13 @@ public override async Task<IReadOnlyList<SExpr>> SendRequestsAndCloseInput(IRead
     }
     var result = new List<SExpr>();
     foreach (var request in requests) {
-      result.Add(await GetProverResponse());
+      result.Add(await GetProverResponse(cancellationToken));
     }
 
     return result;
   }
 
-  protected virtual Task<SExpr> GetProverResponse()
+  protected virtual Task<SExpr> GetProverResponse(CancellationToken cancellationToken = default)
   {
     return Task.FromResult(responses.Count > 0 ? responses.Dequeue() : null);
   }

Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs

@@ -217,7 +217,7 @@ public async Task<SolverOutcome> CheckSat(CancellationToken cancellationToken,
           {
             if (usingUnsatCore)
             {
-              var resp = await SendVcRequest("(get-unsat-core)").WaitAsync(cancellationToken);
+              var resp = await SendVcRequest("(get-unsat-core)", cancellationToken).WaitAsync(cancellationToken);
               ReportCoveredElements(resp);
             }
           }
@@ -285,7 +285,7 @@ public async Task<SolverOutcome> CheckSat(CancellationToken cancellationToken,
     }
 
     // TODO seems like there's a sort of empty line being returned that we can use to check that the solver is done, but this code doesn't use it.
-    private Task<SExpr> SendVcRequest(string s) {
+    private Task<SExpr> SendVcRequest(string s, CancellationToken cancellationToken = default) {
       s = Sanitize(s);
 
       if (currentLogFile != null)
@@ -294,7 +294,7 @@ private Task<SExpr> SendVcRequest(string s) {
         currentLogFile.Flush();
       }
 
-      return Process.SendRequest(s);
+      return Process.SendRequest(s, cancellationToken);
     }
 
     private T WrapInPushPop<T>(ref bool popLater, Func<T> action)
@@ -493,7 +493,7 @@ private async Task<Model> GetErrorModel(CancellationToken cancellationToken)
         return null;
       }
 
-      var resp = await SendVcRequest("(get-model)").WaitAsync(cancellationToken);
+      var resp = await SendVcRequest("(get-model)", cancellationToken).WaitAsync(cancellationToken);
       return resp != null ? ParseErrorModel(resp) : null;
     }
 
@@ -502,15 +502,15 @@ private async Task<SolverOutcome> CheckSatAndGetResponse(CancellationToken cance
       var result = SolverOutcome.Undetermined;
       var wasUnknown = false;
 
-      var checkSatResponse = await SendVcRequest("(check-sat)").WaitAsync(cancellationToken);
+      var checkSatResponse = await SendVcRequest("(check-sat)", cancellationToken).WaitAsync(cancellationToken);
       if (checkSatResponse != null)
       {
         result = ParseOutcome(checkSatResponse, out wasUnknown);
       }
 
       if (wasUnknown)
       {
-        var getInfoResponse = await SendVcRequest("(get-info :reason-unknown)").WaitAsync(cancellationToken);
+        var getInfoResponse = await SendVcRequest("(get-info :reason-unknown)", cancellationToken).WaitAsync(cancellationToken);
         if (getInfoResponse != null)
         {
           result = ParseReasonUnknown(getInfoResponse, result);
@@ -521,7 +521,7 @@ private async Task<SolverOutcome> CheckSatAndGetResponse(CancellationToken cance
       }
 
       if (options.Solver == SolverKind.Z3) {
-        resourceCount = ParseRCount(await SendVcRequest($"(get-info :{Z3.RlimitOption})"));
+        resourceCount = ParseRCount(await SendVcRequest($"(get-info :{Z3.RlimitOption})", cancellationToken));
         // Sometimes Z3 doesn't tell us that it ran out of resources
         if (result != SolverOutcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) {
           result = SolverOutcome.OutOfResource;
@@ -716,7 +716,7 @@ public override int GetRCount()
         }
 
         Contract.Assert(usingUnsatCore, "SMTLib prover not setup for computing unsat cores");
-        var resp = await SendVcRequest("(get-unsat-core)").WaitAsync(cancellationToken);
+        var resp = await SendVcRequest("(get-unsat-core)", cancellationToken).WaitAsync(cancellationToken);
         var unsatCore = new List<int>();
         if (resp is not null && resp.Name != "")
         {
@@ -812,7 +812,7 @@ public override int GetRCount()
         {
           foreach (var relaxVar in relaxVars)
           {
-            var resp = await SendVcRequest($"(get-value ({relaxVar}))").WaitAsync(cancellationToken);
+            var resp = await SendVcRequest($"(get-value ({relaxVar}))", cancellationToken).WaitAsync(cancellationToken);
             if (resp == null)
             {
               break;

Source/Provers/SMTLib/UnsatSolver.cs

@@ -25,10 +25,18 @@ public override void Send(string request)
   }
 
 
-  protected override async Task<SExpr> GetProverResponse() {
-    if (responses.Peek().Name == "unsat") {
-      await semaphore.WaitAsync();
+  protected override async Task<SExpr> GetProverResponse(CancellationToken cancellationToken = default) {
+    if (responses.Count > 0 && responses.Peek().Name == "unsat") {
+      try {
+        await semaphore.WaitAsync(cancellationToken);
+      }
+      catch (OperationCanceledException) {
+        // Discard the response this request enqueued so later requests on this
+        // solver don't pick up a stale "unsat" from a cancelled check-sat.
+        responses.Dequeue();
+        throw;
+      }
     }
-    return await base.GetProverResponse();
+    return await base.GetProverResponse(cancellationToken);
   }
 }

Source/VCGeneration/BlockTransformations.cs

@@ -16,12 +16,21 @@ public static void Optimize(IList<Block> blocks) {
     foreach (var block in blocks)
     {
       // make blocks ending in assume false leaves of the CFG-DAG
-      StopControlFlowAtAssumeFalse(block); 
+      StopControlFlowAtAssumeFalse(block);
     }
 
     DeleteBlocksNotLeadingToAssertions(blocks);
     DeleteStraightLineBlocksWithoutCommands(blocks);
     BlockCoalescer.CoalesceInPlace(blocks);
+    // DeleteBlocksNotLeadingToAssertions rewrites gotos without touching
+    // Predecessors, and BlockCoalescer replaces a block's TransferCmd with its
+    // absorbed successor's without updating the downstream Predecessors either.
+    // Downstream code (notably Split.DoSplit and Split.CountAssertions) relies on
+    // Predecessors matching the final CFG, so rebuild them here.
+    foreach (var block in blocks) {
+      block.Predecessors.Clear();
+    }
+    Implementation.ComputePredecessorsForBlocks(blocks);
   }
 
   private static void StopControlFlowAtAssumeFalse(Block block)

Source/VCGeneration/Splits/SplitAndVerifyWorker.cs

@@ -142,6 +142,19 @@ async Task DoWork(int iteration, Split split, CancellationToken cancellationToke
           totalProverElapsedTime += checker.ProverRunTime;
         }
       }
+      catch (TimeoutException)
+      {
+        // The belt-and-suspenders WaitAsync timeout in StartCheck fired, usually
+        // because the prover subprocess is stuck (e.g. left in a bad state by a
+        // previous malformed SMT query). Reset the checker and record the split
+        // as timed out instead of propagating the exception out of verification.
+        await checker.GoBackToIdle();
+        lock (this)
+        {
+          vcOutcome = MergeOutcomes(vcOutcome, SolverOutcome.TimeOut);
+        }
+        callback.OnTimeout("prover did not respond within timeout");
+      }
       catch
       {
         await checker.GoBackToIdle();