Merge pull request #14 from cpitclaudel/clean-prover-exit

Stop truncating the prover logs

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();

     }