Struct Report 

pub struct Report {
    pub result: Option<i64>,
    pub runs: usize,
    pub flips_verified: usize,
    pub sinks: Vec<SinkRec>,
    pub properties: Vec<PropertyRec>,
    pub flips: Vec<FlipRec>,
    pub gaps: Vec<String>,
    pub exhausted: bool,
}

The session report - the architecture-neutral subset of the engine report that a consumer (a diagnosis layer, a CI gate, a notebook) reads.

Fields

result: Option<i64>

The base run’s result, when it returned.

runs: usize

Concrete runs attempted, including attempts that failed at the engine level.

flips_verified: usize

Flips the reference engine verified.

sinks: Vec<SinkRec>

Sinks reached.

properties: Vec<PropertyRec>

Property queries posed.

flips: Vec<FlipRec>

Every flip attempt.

gaps: Vec<String>

Gap notes, verbatim: the frontend’s own walk notes plus the loop’s own limit notes (run failed: ..., run trapped: ..., walk could not replay ..., solver Unknown at ...).

exhausted: bool

The frontier emptied with no work left undone. A session whose budget cut the decision loop short, refused a property verification, or could not walk a discovered path is NOT exhausted, even if every path it did process was processed to the end.

Trait Implementations

impl Clone for Report

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Report

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Report

fn default() -> Self

Returns the “default value” for a type.