Exception in solver interaction leads to false report of validity

[atomb]

If exceptions arise during interaction with a solver, VCGen.VerifyImplementation can sometimes silently and erroneously return Correct. In particular, I've seen this arise twice:

• When incorrectly implementing a new feature in NoopSolver that led to an exception in SMTLibProcessTheoremProver.GetRCount.
• When attempting to use Dafny with Yices and configuring it incorrectly.

You can replicate this by putting the following in an executable file named badz3:

#!/bin/bash
echo "dfksal"

And then running Boogie with the prover set to that script, something like this:

dotnet Source/BoogieDriver/bin/Debug/net6.0/BoogieDriver.dll /trace /proverOpt:PROVER_PATH=`pwd`/badz3 Test/test2/Arrays.bpl

This leads to the following output:

Parsing Test/test2/Arrays.bpl
Coalescing blocks...
Inlining...
[TRACE] Using prover: /Users/aarotomb/Repositories/boogie/badz3

Verifying P0 ...
  [0.101 s, 2 proof obligations]  verified

Verifying P1 ...
  [0.001 s, 1 proof obligation]  verified

Verifying P2 ...
  [0.000 s, 1 proof obligation]  verified

Verifying Q0 ...
  [0.001 s, 2 proof obligations]  verified

Verifying Q1 ...
  [0.000 s, 1 proof obligation]  verified

Verifying Q2 ...
  [0.000 s, 1 proof obligation]  verified

Verifying Q3 ...
  [0.000 s, 1 proof obligation]  verified

Verifying Q4 ...
  [0.000 s, 1 proof obligation]  verified

Verifying Skip0 ...
  [0.000 s, 2 proof obligations]  verified

Verifying Skip1 ...
  [0.001 s, 2 proof obligations]  verified

Boogie program verifier finished with 10 verified, 0 errors

When running with a working Z3, it reports 8 verified, 2 errors.

I believe that the issue arises at least in part from the following line:

boogie/Source/VCGeneration/VCGen.cs

Line 839 in da30caa

Outcome outcome = Outcome.Correct;

I was hoping that changing Correct to Inconclusive here would resolve the issue, and that later code would set the outcome to Correct when encountering concrete evidence of correctness (e.g., "unsat" from a prover). However, it seems as though later code depends on this initial value, so I'm still investigating the appropriate fix.

[keyboardDrummer]

I can also get Boogie to return "Verified" if I run it in Zsh and use "Ctrl+C" to terminate the process.

[atomb]

Closed by #488.