Stop truncating the prover logs

As it stands, Boogie abruptly aborts the prover by calling Kill() on the
associated process after receiving responses to all of its queries. In
most cases this is fine, but in general this is pretty bad: it yields to
all sorts of output corruption when user-supplied options require z3 to
write output to an auxiliary file (say, using /z3opt:TRACE=true). This
explains why VCC's Axiom Profiler often complains about a missing [eof]
after running Boogie with /z3opt:TRACE=true.

This patch fixes it by only falling back to Kill if the process seems to
have become unresponsive. That is, it starts by cleanly closing the
process input, which signals the end of the interactive session. It then
waits for a clean exit for 2s, and only after that does it resort to
calling Kill(). I've striven for minimal modifications to the logic, so
the patch still universally swallows errors that might occur while
closing the underlying stream, and still calls Kill() (I wouldn't be
against Boogie just hanging if z3 hangs too).

On my tests, z3 exits cleanly pretty much instantly after input is closed
anyway, so I don't expect the timeout to fire often (which would be one
more reason to actually remove that timeout, and condition Boogie's exit
on that of z3 IMO).

1 files changed, 14 insertions, 5 deletions

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 4a1331c5..7776f4de 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -80,10 +80,22 @@ namespace Microsoft.Boogie.SMTLib
     void ControlCHandler(object o, ConsoleCancelEventArgs a)

     {

       if (prover != null) {

-        prover.Kill();

+        TerminateProver();

       }

     }

 

+    private void TerminateProver(Int32 timeout = 2000) {

+      try {

+        // Let the prover know that we're done sending input.

+        prover.StandardInput.Close();

+

+         // Give it a chance to exit cleanly (e.g. to flush buffers)

+        if (!prover.WaitForExit(timeout)) {

+          prover.Kill();

+        }

+      } catch { /* Swallow errors */ }

+    }

+

     public void Send(string cmd)

     {

       if (options.Verbosity >= 2) {

@@ -180,10 +192,7 @@ namespace Microsoft.Boogie.SMTLib
     public void Close()

     {

       TotalUserTime += prover.UserProcessorTime;

-      try {

-        prover.Kill();

-      } catch {

-      }

+      TerminateProver();

       DisposeProver();

     }