Skip to main content

with_verification_context

synth_verify

Function with_verification_context 

Source 
pub fn with_verification_context<F, R>(f: F) -> R
where
    F: FnOnce() -> R + Send + Sync,
    R: Send + Sync,
Expand description

Run verification operations in a configured context.

With the default (ordeal) engine this is a plain call — the pure-Rust solver needs no global context. With the z3-solver feature compiled in, it additionally configures the Z3 thread-local context (30-second timeout, model generation) so the differential oracle is ready.