Struct VerificationCondition 

pub struct VerificationCondition {
    pub name: String,
    pub kind: VcKind,
    pub declarations: Vec<SmtDecl>,
    pub assumes: Vec<Spanned<Expr>>,
    pub goals: Vec<Spanned<Expr>>,
    pub safety_rules: Vec<SafetySource>,
    pub unsupported: Option<String>,
}

A verification condition to be checked by SMT.

Fields

name: String

kind: VcKind

declarations: Vec<SmtDecl>

Declarations needed (types, uninterpreted functions).

assumes: Vec<Spanned<Expr>>

Assertions: requires + invariants(unprimed).

goals: Vec<Spanned<Expr>>

Goal: ensures + invariants(as written, may contain primes).

safety_rules: Vec<SafetySource>

Safety rules merged from safety declarations.

unsupported: Option<String>

If set, this VC cannot be encoded yet — reason string.

Trait Implementations

impl Clone for VerificationCondition

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for VerificationCondition

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

Formats the value using the given formatter.