Fix issue #322

boogie-org · Dec 24, 2020 · f2f75fd · f2f75fd
1 parent 76016d5
commit f2f75fd
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 7 deletions.
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
@@ -181,7 +181,7 @@ private string ConfirmProverPath(string proverPath)
     protected void ReportError(string msg)
     {
       Contract.Requires(msg != null);
-      throw new ProverOptionException(msg + "\n\n" + Help);
+      throw new ProverOptionException(msg);
     }
 
     protected virtual bool ParseString(string opt, string name, ref string field)
@@ -341,7 +341,7 @@ public ProverException(string s)
     }
   }
 
-  public class ProverOptionException : Exception
+  public class ProverOptionException : ProverException
   {
     public ProverOptionException(string msg)
       : base(msg)

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1027,16 +1027,14 @@ public static PipelineOutcome InferAndVerify(Program program,
       {
         ae.Handle(e =>
         {
-          var pe = e as ProverException;
-          if (pe != null)
+          if (e is ProverException)
           {
-            printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e);
+            printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e.Message);
             outcome = PipelineOutcome.FatalError;
             return true;
           }
 
-          var oce = e as OperationCanceledException;
-          if (oce != null)
+          if (e is OperationCanceledException)
           {
             return true;
           }

diff --git a/Test/prover/issue-322.bpl b/Test/prover/issue-322.bpl
@@ -0,0 +1,5 @@
+// RUN: %boogie -proverOpt:PROVER_PATH=bogus-path "%s" > "%t"
+// RUN: %boogie -proverOpt:bogus-option "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure foo() {}
diff --git a/Test/prover/issue-322.bpl.expect b/Test/prover/issue-322.bpl.expect
@@ -0,0 +1,2 @@
+Fatal Error: ProverException: Cannot find specified prover: bogus-path
+Fatal Error: ProverException: Unrecognised prover option: bogus-option
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		Fatal Error: ProverException: Cannot find specified prover: bogus-path
		Fatal Error: ProverException: Unrecognised prover option: bogus-option