Struct EquivalenceResult 

pub struct EquivalenceResult {
    pub equivalent: bool,
    pub counterexample: Option<Vec<(String, String)>>,
    pub bound: u32,
}

Result of checking semantic equivalence between FOL and SVA.

Fields

equivalent: bool

Whether the properties are equivalent at the given bound.

counterexample: Option<Vec<(String, String)>>

If not equivalent, counterexample signal assignments (name@timestep → value).

bound: u32

The BMC bound used for checking.

Trait Implementations

impl Debug for EquivalenceResult

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

Formats the value using the given formatter.