Struct CounterExample 

pub struct CounterExample {
    pub assignments: Vec<(String, String)>,
}

A counterexample showing concrete values that falsify an assertion.

When Z3 finds that an assertion is not valid, it produces a model (set of variable assignments) that makes the negation of the assertion true. This counterexample helps users understand exactly why verification failed.

Example Interpretation

If verifying x > 5 fails with counterexample x = 3, this means:

• The solver found that x = 3 is a possible value
• With x = 3, the assertion x > 5 is false
• Therefore the assertion is not universally valid

Fields

assignments: Vec<(String, String)>

Variable assignments that make the assertion false.

Each tuple contains (variable_name, value_as_string).

Trait Implementations

impl Clone for CounterExample

fn clone(&self) -> CounterExample

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CounterExample

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

Formats the value using the given formatter.

impl Display for CounterExample

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

Formats the value using the given formatter.