From 0fbcdbb8b039fd01346e51d5dd37a58974c1329f Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 26 Apr 2023 14:13:22 +0200
Subject: [PATCH 1/2] Prevent Boogie from hanging when an exception occurs when
 acquiring a checker, which can occur of the solver path is incorrect or the
 solver doesn't function correctly

---
 Source/VCGeneration/CheckerPool.cs                 | 14 +++++++++-----
 .../broken_solver_more_impls_than_cores.bpl        | 12 ++++++++++++
 .../broken_solver_more_impls_than_cores.bpl.expect |  1 +
 3 files changed, 22 insertions(+), 5 deletions(-)
 create mode 100644 Test/commandline/broken_solver_more_impls_than_cores.bpl
 create mode 100644 Test/commandline/broken_solver_more_impls_than_cores.bpl.expect

diff --git a/Source/VCGeneration/CheckerPool.cs b/Source/VCGeneration/CheckerPool.cs
index e4c451821..7c9cc52a4 100644
--- a/Source/VCGeneration/CheckerPool.cs
+++ b/Source/VCGeneration/CheckerPool.cs
@@ -28,12 +28,16 @@ public async Task<Checker> FindCheckerFor(ConditionGeneration vcgen, Split? spli
       }
 
       await checkersSemaphore.WaitAsync(cancellationToken);
-      if (!availableCheckers.TryTake(out var checker)) {
-        checker ??= CreateNewChecker();
+      try {
+        if (!availableCheckers.TryTake(out var checker)) {
+          checker ??= CreateNewChecker();
+        }
+        PrepareChecker(vcgen.program, split, checker);
+        return checker;
+      } catch (Exception) {
+        checkersSemaphore.Release();
+        throw;
       }
-
-      PrepareChecker(vcgen.program, split, checker);
-      return checker;
     }
 
     private int createdCheckers;
diff --git a/Test/commandline/broken_solver_more_impls_than_cores.bpl b/Test/commandline/broken_solver_more_impls_than_cores.bpl
new file mode 100644
index 000000000..1cd606ad4
--- /dev/null
+++ b/Test/commandline/broken_solver_more_impls_than_cores.bpl
@@ -0,0 +1,12 @@
+// RUN: ! %boogie /vcsCores:1 "/proverOpt:PROVER_PATH=doesNotExit" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure first()
+{
+    assume true;
+}
+
+procedure second()
+{
+    assume true;
+}
\ No newline at end of file
diff --git a/Test/commandline/broken_solver_more_impls_than_cores.bpl.expect b/Test/commandline/broken_solver_more_impls_than_cores.bpl.expect
new file mode 100644
index 000000000..825b20418
--- /dev/null
+++ b/Test/commandline/broken_solver_more_impls_than_cores.bpl.expect
@@ -0,0 +1 @@
+Fatal Error: ProverException: Cannot find specified prover: doesNotExit

From 12bd99cc90e916ebe5bb72023c4d44af939a54a5 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 26 Apr 2023 14:14:43 +0200
Subject: [PATCH 2/2] Bump version number

---
 Source/Directory.Build.props | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
index 25b3283a0..b86754e12 100644
--- a/Source/Directory.Build.props
+++ b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>2.16.5</Version>
+    <Version>2.16.6</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>