Function run_minion_parallel 

pub fn run_minion_parallel(
    num_threads: usize,
    model: Model,
    callback: ParallelCallback<'_>,
) -> Result<(), MinionError>

Run Minion as a portfolio search across num_threads worker threads.

Each thread builds its own solver from a shared Model, with a derived random seed; the first thread to find sollimit solutions (or to prove unsat) signals the others to stop. The callback is invoked at most once per solution found by any worker, serialised internally so it never re-enters itself.

num_threads must be >= 1. With num_threads == 1 behaviour is equivalent to a sequential run_minion.

Mid-search mutation is NOT supported in this mode (each worker has its own context; mutating one wouldn’t propagate). Use the sequential run_minion_midsearch path if you need that.

Concurrency

run_minion_parallel itself spawns OS threads internally. It is safe to call from a single thread of the host process per call, but it is not safe to invoke from multiple host threads concurrently — the underlying Minion alarm/ctrl-C handlers are per-process and racing threaded runs can corrupt them. (The fork-based -parallel flag has the same constraint at the process level.) For sequential use across many models, just call this function repeatedly.