Function write_failure 

fn write_failure(
    s: &mut String,
    failure: &InvariantFailure,
    name_suffix: &str,
) -> bool

Appends [FAIL: reason]{name_suffix} plus the counterexample sequence, if any.

Returns true if a sequence (ending in a newline) was written.