Kill the solver process when ctrl-c is pressed

1 files changed, 26 insertions, 3 deletions

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index b23fddbb..d2038d70 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -21,7 +21,8 @@ namespace Microsoft.Boogie.SMTLib
     readonly SMTLibProverOptions options;

     readonly Queue<string> proverOutput = new Queue<string>();

     readonly Queue<string> proverErrors = new Queue<string>();

-    readonly TextWriter toProver;    

+    readonly TextWriter toProver;

+    ConsoleCancelEventHandler cancelEvent;

 

     public static ProcessStartInfo ComputerProcessStartInfo(string executable, string options)

     {

@@ -39,6 +40,11 @@ namespace Microsoft.Boogie.SMTLib
     {

       this.options = options;

 

+      if (cancelEvent == null && CommandLineOptions.Clo.RunningBoogieFromCommandLine) {

+        cancelEvent = new ConsoleCancelEventHandler(ControlCHandler);

+        Console.CancelKeyPress += cancelEvent;

+      }

+

       try {

         prover = Process.Start(psi);

         prover.ErrorDataReceived += prover_ErrorDataReceived;

@@ -51,6 +57,14 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

+    [NoDefaultContract]  // important, since we have no idea what state the object might be in when this handler is invoked

+    void ControlCHandler(object o, ConsoleCancelEventArgs a)

+    {

+      if (prover != null) {

+        prover.Kill();

+      }

+    }

+

     public void Send(string cmd)

     {

       if (options.Verbosity >= 2) {

@@ -257,12 +271,22 @@ namespace Microsoft.Boogie.SMTLib
             return proverOutput.Dequeue();

           }

 

-          if (prover.HasExited)

+          if (prover.HasExited) {

+            DisposeProver();

             return null;

+          }

         }

       }

     }

 

+    void DisposeProver()

+    {

+      if (cancelEvent != null) {

+        Console.CancelKeyPress -= cancelEvent;

+        cancelEvent = null;

+      }

+    }

+

     void prover_OutputDataReceived(object sender, DataReceivedEventArgs e)

     {

       lock (this) {

@@ -288,7 +312,6 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

     #endregion

-

   }

 }