Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP provers. Add handling of help message about /proverOpt.

1 files changed, 5 insertions, 5 deletions

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index af9668d4..9fd87127 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -123,7 +123,7 @@ void ObjectInvariant()
              base.Parse(opt);

     }

 

-    protected override void PostParse()

+    public override void PostParse()

     {

       base.PostParse();

 

@@ -133,12 +133,11 @@ void ObjectInvariant()
       }     

     }

 

-    public string Help

+    public override string Help

     {

       get

       {

-          return

-              // base.Help +

+        return

 @"

 Z3-specific options:

 ~~~~~~~~~~~~~~~~~~~~

@@ -149,7 +148,8 @@ Obscure options:
 ~~~~~~~~~~~~~~~~

 DIST=<bool>               Use z3-dist.exe binary.

 REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.

-";

+

+" + base.Help;

           // DIST requires non-public binaries

       }

     }