# Z3 Parallel Solving + Multi-Solver Portfolio for fold

> Generated 2026-05-29. Research on accelerating fold's Z3 solving.

## Current State

fold uses `z3::solver` with `QF_BV` logic. The `--portfolio` flag runs Z3 tactics in parallel threads (bit-blast + SAT). Default per-query timeout is 2000ms.

## Multi-Solver Portfolio Opportunity

| Solver | BV perf vs Z3 | Language | Integration |
|--------|--------------|----------|-------------|
| **Bitwuzla** | 5.1x faster | C/C++ | C API, drop-in for Z3 |
| CVC5 | ~3x slower | C++ | C API, broader theory support |
| MathSAT | Similar | C | C API, optimization (OMT) |

**Recommended**: Add `--solver bitwuzla` flag to fold. On BV-only queries (which fold uses exclusively), Bitwuzla is 5x faster. Keep Z3 as default for its mature tactics engine, but offer Bitwuzla for large codebases.

## Incremental Solving

fold already uses `solver.push()`/`solver.pop()` in the security walker for branch-local constraints. Z3's incremental mode reuses learned clauses across queries — fold leverages this implicitly.

## Parallel Portfolio (ESBMC Pattern)

ESBMC dispatches to 6 solvers simultaneously and returns the first result. fold's current `checkWithPortfolio` uses Z3 tactics only. Could extend to:

```cpp
// Dispatch to Z3, Bitwuzla, and CVC5 in parallel
auto result = race({
    z3_solver.check(assumptions),
    bitwuzla_solver.check(assumptions),
    cvc5_solver.check(assumptions)
});
```

This trades memory for speed — 3 solvers running simultaneously on different cores.

## Bitwuzla Integration Plan

1. Add `--solver` flag to ScanOptions (choices: z3, bitwuzla, portfolio-all)
2. Add Bitwuzla C API wrapper in `src/symbolic/bitwuzla_solver.cpp`
3. Extend `checkWithPortfolio` in `tactics.cpp` to optionally dispatch to Bitwuzla
4. Benchmark on fold's own codebase to measure speedup

**Expected impact**: 2-5x speedup on BV-heavy queries. Most fold queries are simple null-equality checks — Bitwuzla's BV specialization is ideal for this workload.