It should be possible to select SAT solver at runtime, not just compiletime

[danielsn]

Currently, as of 5.73, you have the choice of building CBMC to use MiniSat or CaDiCaL as a solver. Each is faster in some cases. However, a user cannot choose on a per-proof basis which to use: they must set the right flag when compiling CBMC then are locked into that choice. This differs from the SMT experience, where you can choose the solver as a commandline flag

Proposal: Add a flag for selecting the SAT solver, just like in SMT

[qinheping]

The CBMC flag --external-sat-solver allow you to choose external sat solver. Is it what you are looking for?

[danielsn]

The issue is that using an external sat solver brings in additional overhead vs a native interface (and afaik incremental solving doesn't work). CBMC has a native interface to CaDiCaL but that is either/or: you either pick minisat or CaDiCaL, but can't get both in the same build.

[martin-cs]

This was on our "Starter tasks" list for years. Run-time switching between the built-ins should be pretty straight-forward.