Unhelpful empty counterexample

[sauclovian-g]

foo.rs:

static X: u32 = 1;

pub fn f() -> u32 {
   X
}

foo.saw, which is incorrect:

enable_experimental;
m <- mir_load_module "foo.linked-mir.json";

let f_spec = do {
    mir_execute_func [];
    mir_return (mir_term {{ 0 : [32] }});
};
mir_verify m "foo::f" [] false f_spec z3;

Running this produces:

[23:36:45.964] Loading file ".../foo.saw"
[23:36:45.996] Verifying foo/b6dd46cd::f[0] ...
[23:36:46.004] Simulating foo/b6dd46cd::f[0] ...
[23:36:46.006] Checking proof obligations foo/b6dd46cd::f[0] ...
[23:36:46.016] Subgoal failed: foo/b6dd46cd::f[0] Literal equality postcondition

[23:36:46.016] SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 227}
[23:36:46.016] ----------Counterexample----------
[23:36:46.016] Stack trace:
"mir_verify" (.../foo.saw:8:1-8:11)
Proof failed.

which sort of tells you what went wrong (though that part could be much clearer) but also prints a 0-line counterexample that will readily confuse the user. If the counterexample is empty we should say something else, like "No counterexample, execution is unconditional".

[RyanGlScott]

We could also be more precise: instead of saying "Literal equality postcondition", we could just say something like "Return value", since that is the specific type of postcondition involved. That make it far more obvious where to look.

Even better would be to say that the expected return value is 0, but the actual return value is 1 (see also #2051).