Function with_z3_context 

pub fn with_z3_context<T: FnOnce() -> R + Send + Sync, R: Send + Sync>(
    ctx: &Context,
    callback: T,
) -> R

Runs the provided callback with all inner Z3 calls using the provided Context.

Requires that the closure and return type be Send and Sync to prevent mixing Z3 objects belonging to multiple Contexts. If you need to move Z3 data into or out of the closure, use PrepareSynchronized::synchronized().

Most users should prefer to use with_z3_config instead; this function is present to allow advanced users to use a Context they unsafely created themselves.

See also

• with_z3_config