Enum TrapVerdict 

pub enum TrapVerdict {
    Preserved,
    Dropped(Vec<(String, u128)>),
    Unknown,
}

The verdict of a trap-preservation gate.

Variants

Preserved

Unsat — the lowering preserves the trap (and, for the full VC, the value). The underlying LRAT certificate re-checked successfully.

Dropped(Vec<(String, u128)>)

Sat — a counterexample input under which the trap was dropped (or spuriously added). Carries the model’s variable → value assignments.

Unknown

Unknown — conservative: do not accept. Also returned if a Preserved certificate fails to re-check (an internal soundness alarm).

Trait Implementations

impl Clone for TrapVerdict

fn clone(&self) -> TrapVerdict

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TrapVerdict

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

Formats the value using the given formatter.

impl Eq for TrapVerdict

impl PartialEq for TrapVerdict

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for TrapVerdict