Enum BmcOutcome 

pub enum BmcOutcome {
    CounterexampleAt {
        k: u32,
        trace: Vec<(String, bool)>,
    },
    NoneWithin(u32),
    Unsupported,
}

The verdict of bounded model checking.

Variants

CounterexampleAt

A reachable state at depth k violates the property, with a witnessing trace.

Fields

k: u32

trace: Vec<(String, bool)>

NoneWithin(u32)

No violating state is reachable within max_k transitions (a bounded guarantee).

Unsupported

An obligation left the propositional fragment — escalate (e.g. bit-blast).

Trait Implementations

impl Clone for BmcOutcome

fn clone(&self) -> BmcOutcome

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BmcOutcome

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

Formats the value using the given formatter.

impl PartialEq for BmcOutcome

fn eq(&self, other: &BmcOutcome) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for BmcOutcome

impl StructuralPartialEq for BmcOutcome