Struct VerificationError 

pub struct VerificationError {
    pub kind: VerificationErrorKind,
    pub span: Option<(usize, usize)>,
    pub explanation: String,
    pub counterexample: Option<CounterExample>,
}

A verification error with Socratic explanation.

Each error includes contextual information to help users understand and fix the issue.

Fields

• kind: Categorizes the error type
• span: Source location (byte offsets) where the error occurred
• explanation: Human-readable context explaining why verification failed
• counterexample: Concrete variable assignments that demonstrate the failure

Fields

kind: VerificationErrorKind

The category of verification error.

span: Option<(usize, usize)>

Optional source span as (start, end) byte offsets.

explanation: String

Human-readable explanation of why verification failed.

counterexample: Option<CounterExample>

Concrete witness showing a failing case, when available.

Implementations

impl VerificationError

pub fn license_required() -> Self

Create a license required error.

Use when verification is attempted without providing a license key.

pub fn license_invalid(reason: impl Into<String>) -> Self

Create a license invalid error.

Use when the provided license key fails validation.

pub fn insufficient_plan(current: impl Into<String>) -> Self

Create an insufficient plan error.

Use when the license is valid but the plan doesn’t include verification.

pub fn contradiction( explanation: impl Into<String>, counterexample: Option<CounterExample>, ) -> Self

Create a contradictory assertion error.

Use when Z3 proves the negation of an assertion is satisfiable.

pub fn bounds_violation( var: impl Into<String>, expected: impl Into<String>, found: impl Into<String>, ) -> Self

Create a bounds violation error.

Use when a variable’s value falls outside its declared constraint.

pub fn refinement_violation( type_name: impl Into<String>, explanation: impl Into<String>, ) -> Self

Create a refinement type violation error.

Use when a value does not satisfy its refinement type predicate.

pub fn solver_unknown() -> Self

Create a solver unknown error.

Use when Z3 cannot determine satisfiability (timeout or undecidable).

pub fn solver_error(message: impl Into<String>) -> Self

Create a solver error.

Use when Z3 encounters an internal error or configuration issue.

pub fn termination_violation( variant: impl Into<String>, reason: impl Into<String>, ) -> Self

Create a termination violation error.

Use when loop termination cannot be proven via the variant expression.

pub fn with_span(self, start: usize, end: usize) -> Self

Set the source span for this error.

Spans are byte offsets (start, end) into the source text.

Trait Implementations

impl Debug for VerificationError

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

Formats the value using the given formatter.

impl Display for VerificationError

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

Formats the value using the given formatter.

impl Error for VerificationError

fn source(&self) -> Option<&(dyn Error + 'static)>

Returns the lower-level source of this error, if any.

fn description(&self) -> &str

👎Deprecated since 1.42.0:

use the Display impl or to_string()

fn cause(&self) -> Option<&dyn Error>

👎Deprecated since 1.33.0:

replaced by Error::source, which can support downcasting

fn provide<'a>(&'a self, request: &mut Request<'a>)

🔬This is a nightly-only experimental API. (error_generic_member_access)

Provides type-based access to context intended for error reports.