Provide /p: as the short form of /proverOpt:.

Add /p:O:<name>=<value> and /p:C:<solver-argument> prover options in SMT.
Add default Z3 options when using Z3.

1 files changed, 18 insertions, 9 deletions

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 8cc67256..b23fddbb 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -71,7 +71,7 @@ namespace Microsoft.Boogie.SMTLib
 

     public bool IsPong(SExpr sx)

     {

-      return sx.Name == ":name";

+      return sx != null && sx.Name == ":name";

     }

 

     public void PingPong()

@@ -79,6 +79,11 @@ namespace Microsoft.Boogie.SMTLib
       Ping();

       while (true) {

         var sx = GetProverResponse();

+        if (sx == null) {

+          ErrorHandler("Prover died");

+          return;

+        }

+

         if (IsPong(sx))

           return;

         else

@@ -261,21 +266,25 @@ namespace Microsoft.Boogie.SMTLib
     void prover_OutputDataReceived(object sender, DataReceivedEventArgs e)

     {

       lock (this) {

-        if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name"))) {

-          Console.WriteLine("[SMT-OUT] {0}", e.Data);

+        if (e.Data != null) {

+          if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name "))) {

+            Console.WriteLine("[SMT-OUT] {0}", e.Data);

+          }

+          proverOutput.Enqueue(e.Data);

+          Monitor.Pulse(this);

         }

-        proverOutput.Enqueue(e.Data);

-        Monitor.Pulse(this);

       }

     }

 

     void prover_ErrorDataReceived(object sender, DataReceivedEventArgs e)

     {

       lock (this) {

-        if (options.Verbosity >= 1)

-          Console.WriteLine("[SMT-ERR] {0}", e.Data);

-        proverErrors.Enqueue(e.Data);

-        Monitor.Pulse(this);

+        if (e.Data != null) {

+          if (options.Verbosity >= 1)

+            Console.WriteLine("[SMT-ERR] {0}", e.Data);

+          proverErrors.Enqueue(e.Data);

+          Monitor.Pulse(this);

+        }

       }

     }

     #endregion