CBMC: Consider systematically employing multiple SMT solver backends for CBMC functions

[mkannwischer]

Identified during the 2026 soundness review (#1582, SOUNDNESS.md).

CBMC relies on an SMT solver backend to discharge verification conditions. Currently, we use a single solver (bitwuzla or Z3). Solver-specific bugs or incompleteness could lead to unsound results going undetected.

Consider systematically running CBMC proofs with multiple SMT solver backends to increase confidence in proof results.