Skip to main content

verify_parameterized

Function verify_parameterized 

Source
pub fn verify_parameterized(
    property: &VerifyExpr,
    parameter: &str,
    param_type: VerifyType,
    constraint: Option<&VerifyExpr>,
) -> ParameterizedResult
Expand description

Verify a parameterized property.

Uses Z3 quantifiers to check: forall param. constraint(param) -> property(param). Falls back to bounded enumeration if quantifier reasoning times out.