Struct SpuriousCounterexample 

pub struct SpuriousCounterexample {
    pub abstract_trace: Vec<String>,
    pub infeasibility_reason: String,
}

A spurious counterexample: an abstract path that has no concrete realization.

Fields

abstract_trace: Vec<String>

The abstract trace (sequence of abstract state descriptions).

infeasibility_reason: String

Why the path is spurious.

Implementations

impl SpuriousCounterexample

pub fn new(trace: Vec<String>, reason: impl Into<String>) -> Self

Create a spurious counterexample.

Trait Implementations

impl Clone for SpuriousCounterexample

fn clone(&self) -> SpuriousCounterexample

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SpuriousCounterexample

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

Formats the value using the given formatter.