Function record_invariant_failure 

fn record_invariant_failure(
    failure_file: &Path,
    call_sequence: &[BaseCounterExample],
    settings: &InvariantSettings,
    assertion_failure: bool,
    storage: &[SymbolicStorageAssignment],
    failure_site: Option<SymbolicInvariantFailureSite>,
)

Persists an invariant failure, with any symbolic replay storage and confirmed failure site.