Skip to main content

collect_quantifier_bound_vars_pub

logicaffeine_verify::equivalence

Function collect_quantifier_bound_vars_pub 

Source 
pub fn collect_quantifier_bound_vars_pub(
    expr: &VerifyExpr,
    int_vars: &mut HashMap<String, Int>,
    bv_vars: &mut HashMap<String, BV>,
    array_vars: &mut HashMap<String, Array>,
)
Expand description

Collect quantifier-bound variables from a VerifyExpr (public API).