Function build_model

crates/openshell-prover/src/model.rs:386–394

Build a reachability model from the given inputs.

(
    policy: PolicyModel,
    credentials: CredentialSet,
    binary_registry: BinaryRegistry,
)

/// Build a reachability model from the given inputs.
pub fn build_model(
    policy: PolicyModel,
    credentials: CredentialSet,
    binary_registry: BinaryRegistry,
) -> ReachabilityModel {
    // Ensure the thread-local Z3 context is initialized
    let _ctx = Context::thread_local();
    ReachabilityModel::new(policy, credentials, binary_registry)
}