Error Localization Based on Inconsistent Models?

[Philipp15b]

Greetings Boogie Team!

I am confused as to why Boogie's error messages that localize verification failures (which assertions fail) are sound. It seems like Boogie uses models from the SMT solver even if the solver returns "unknown".

From Z3Prover/z3#4924, I understand that Boogie needs to have a model from the SMT solver to give error messages, and will use models even from "unknown" SMT queries.
In Boogie's source code, I see that an "unknown" result will be converted to a SolverOutcome.Invalid (reference 1), and in this case the (potentially inconsistent) model from the SMT solver is used anyway (reference 2).

For counter-examples (inputs to the program to fail verification), Dafny has an explicit option to enable those and warnings have been added regarding possible inconsistencies (references 3). Based on my naive understanding of Boogie's verification, the same SMT models are used for both counter-examples and error localization.

However, I have not found a warning about potential unsoundness of the error localization. It is also enabled by default, in contrast to the counter-examples.

What soundness guarantees are there for the error localization in Boogie?

Any clarification would be much appreciated!

References:

1. boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

   Line 1184 in 2af8e63

   protected SolverOutcome ParseOutcome(SExpr resp, out bool wasUnknown)

2. boogie/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs

   Line 234 in 2af8e63

   if (result == SolverOutcome.Invalid)

3. Counter-Examples section in Dafny Guide, explanatory footnote in Dafny Guide, Counterexamples As Assumptions dafny-lang/dafny#5013 (comment)).

[shazqadeer]

I am confused as to why Boogie's error messages that localize verification failures (which assertions fail) are sound. It seems like Boogie uses models from the SMT solver even if the solver returns "unknown".

That is correct. Boogie does not distinguish between "unknown" and "sat" from the underlying SMT solver.

There are no guarantees when Boogie returns an error. Having said that, if your input file does not have quantifiers, you can expect the error to be a real one and to be localized correctly.