diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs index deeb66b54..43dda6925 100644 --- a/Source/ExecutionEngine/VerificationTask.cs +++ b/Source/ExecutionEngine/VerificationTask.cs @@ -89,6 +89,8 @@ public void Cancel() { StartRun(cancellationSource.Token).ToObservable(). Catch(_ => Observable.Return(new Stale())). + Catch(e => cancellationSource.IsCancellationRequested + ? Observable.Return(new Stale()) : Observable.Throw(e)). Subscribe(next => { status.OnNext(next); }, e => { @@ -115,8 +117,8 @@ public void Cancel() { private async IAsyncEnumerable StartRun([EnumeratorCancellation] CancellationToken cancellationToken) { var timeout = Split.Run.Implementation.GetTimeLimit(Split.Options); - - var checkerTask = engine.CheckerPool.FindCheckerFor(ProcessedProgram.Program, Split, CancellationToken.None); + + var checkerTask = engine.CheckerPool.FindCheckerFor(ProcessedProgram.Program, Split, cancellationToken); if (!checkerTask.IsCompleted) { yield return new Queued(); } diff --git a/Source/VCGeneration/CheckerPool.cs b/Source/VCGeneration/CheckerPool.cs index b75744377..0f4f45353 100644 --- a/Source/VCGeneration/CheckerPool.cs +++ b/Source/VCGeneration/CheckerPool.cs @@ -23,10 +23,6 @@ public CheckerPool(VCGenOptions options) public async Task FindCheckerFor(Program program, Split? split, CancellationToken cancellationToken) { - if (disposed) { - throw new Exception("CheckerPool was already disposed"); - } - await checkersSemaphore.WaitAsync(cancellationToken); try { if (!availableCheckers.TryPop(out var checker)) { @@ -43,6 +39,11 @@ public async Task FindCheckerFor(Program program, Split? split, Cancell private int createdCheckers; private Checker CreateNewChecker() { + if (disposed) + { + throw new ObjectDisposedException(nameof(CheckerPool)); + } + var log = Options.ProverLogFilePath; var index = Interlocked.Increment(ref createdCheckers) - 1; if (log != null && !log.Contains("@PROC@") && index > 0) { @@ -57,6 +58,7 @@ public void Dispose() lock(availableCheckers) { disposed = true; + checkersSemaphore.Dispose(); while (availableCheckers.TryPop(out var checker)) { checker.Close(); }