verify_with_z3

rapx::analysis::senryx::symbolic_analysis

Function verify_with_z3 

Source 
pub fn verify_with_z3<'tcx, F>(
    values: HashMap<usize, ValueDomain<'tcx>>,
    path_constraints: Vec<SymbolicDef<'tcx>>,
    target_verifier: F,
) -> bool
where
    F: for<'ctx> FnOnce(&'ctx Context, &HashMap<usize, BV<'ctx>>) -> Bool<'ctx>,
Expand description

Verifies a target property using Z3 SMT solver given variable domains and path constraints. Returns true if the property holds (UNSAT for negation), false otherwise.