Enum VerificationErrorKind 

pub enum VerificationErrorKind {
    ContradictoryAssertion,
    BoundsViolation {
        var: String,
        expected: String,
        found: String,
    },
    RefinementViolation {
        type_name: String,
    },
    LicenseRequired,
    LicenseInvalid {
        reason: String,
    },
    LicenseInsufficientPlan {
        current: String,
    },
    SolverUnknown,
    SolverError {
        message: String,
    },
    TerminationViolation {
        variant: String,
        reason: String,
    },
}

The category of verification error.

Each variant represents a distinct failure mode with specific remediation steps.

Variants

ContradictoryAssertion

An assertion that can never be true.

Z3 proved that no interpretation satisfies the assertion.

Common causes:

• Conflicting constraints (e.g., x > 5 and x < 3)
• Logical contradictions in premises
• Impossible refinement type predicates

Action: Review your assumptions for conflicts.

BoundsViolation

A variable violates its declared bounds.

The verifier found a possible value that falls outside the declared constraint.

Action: Either tighten the constraint or add assumptions that rule out the violating value.

Fields

var: String

The variable that violated its bounds.

expected: String

The constraint that was expected.

found: String

The value that violated the constraint.

RefinementViolation

A refinement type predicate is not satisfied.

The value being assigned does not satisfy the predicate in the refinement type definition.

Action: Ensure the value meets the refinement predicate, or add assumptions that constrain the value appropriately.

Fields

type_name: String

The name of the refinement type.

LicenseRequired

Verification requires a license key.

Action: Provide a license key via --license <key> or the LOGOS_LICENSE environment variable.

LicenseInvalid

The license key is invalid or expired.

Action: Check that your license key is correct and active.

Fields

reason: String

The reason the license was rejected.

LicenseInsufficientPlan

The license plan doesn’t include verification.

Verification requires Pro, Premium, Lifetime, or Enterprise plan.

Action: Upgrade your plan at https://logicaffeine.com/pricing.

Fields

current: String

The user’s current plan.

SolverUnknown

Z3 returned unknown (timeout or undecidable).

The solver could not determine validity within the timeout period, or the problem is undecidable.

Action: Simplify the assertion or add more constraining assumptions.

SolverError

Z3 initialization or internal error.

An unexpected error occurred in the Z3 solver.

Action: Check that Z3 is properly installed and configured.

Fields

message: String

The error message from Z3.

TerminationViolation

Loop termination cannot be proven.

The verifier could not prove that the loop variant strictly decreases on each iteration while remaining non-negative.

Action: Ensure your variant expression decreases by at least 1 on each iteration and has a lower bound.

Fields

variant: String

The variant expression that should decrease.

reason: String

Why termination could not be proven.

Trait Implementations

impl Clone for VerificationErrorKind

fn clone(&self) -> VerificationErrorKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for VerificationErrorKind

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

Formats the value using the given formatter.

impl PartialEq for VerificationErrorKind

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for VerificationErrorKind