Fix hanging when solver exits with a non-zero exit code (#821)

Previously, if the solver quit abruptly with a non-zero exit code (such as for a segmentation fault), Boogie would hang. These changes turn that into a well-behaved solver exception. --------- Co-authored-by: Remy Willems <[email protected]>
boogie-org · Dec 6, 2023 · 4896769 · 4896769
1 parent c545628
commit 4896769
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 1 deletion.
diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.0.8</Version>
+    <Version>3.0.9</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -58,6 +58,7 @@ public SMTLibProcess(SMTLibOptions libOptions, SMTLibSolverOptions options)
       {
         solver = new Process();
         solver.StartInfo = psi;
+        solver.EnableRaisingEvents = true;
         solver.ErrorDataReceived += SolverErrorDataReceived;
         solver.OutputDataReceived += SolverOutputDataReceived;
         solver.Exited += SolverExited;
@@ -74,6 +75,10 @@ public SMTLibProcess(SMTLibOptions libOptions, SMTLibSolverOptions options)
 
     private void SolverExited(object sender, EventArgs e)
     {
+      if (options.Verbosity >= 2) {
+        Console.WriteLine($"[SMT-ERR-{{0}}] Solver exited with code {solver.ExitCode}.");
+      }
+
       lock (this) {
         while (outputReceivers.TryDequeue(out var source)) {
           source.SetResult(null);

diff --git a/Test/prover/exitcode.bpl b/Test/prover/exitcode.bpl
@@ -0,0 +1,8 @@
+// RUN: %parallel-boogie /proverOpt:PROVER_PATH=/usr/bin/false "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK: exitcode.bpl\(6,11\): Verification encountered solver exception \(P\)
+// CHECK: Boogie program verifier finished with 0 verified, 0 errors, 1 solver exceptions
+
+procedure P(x: int, y: int) {
+  assert x*y == y*x;
+}