Introduce --prover-option flag for CBMC

[rod-chapman]

I propose the main "cbmc" command should introduce a new

--prover-option=XXX

command-line option. If specified, then "XXX" is passed to the underlying prover (whichever one it is) to offer a little more control of its behaviour.

For example

cbmc --smt2 --prover-option="tactic.default_tactic=smt" mything.goto

would invoke

z3 tactic.default_tactic=smt ...

under the hood, and similarly for other provers like bitwuzla, cadical, etc. etc.

[rod-chapman]

I also suggest that, if more than one of these options is given, then the parameters are passed on to the prover in that order.
e.g.

cbmc --smt2 --prover-option=XXX --prover-option=YYY ...

invokes

z3 XXX YYY ...

and so on...

[kroening]

Rod: how about --external-smt-solver binary, to get some symmetry to --external-sat-solver. You would then be able to
a) point to a script that has arbitrary logic in it to determine the right command line options for your solver.
b) be able to use multiple versions of z3, to get the one with the heuristic you want.

[rod-chapman]

Not sure .. we pull in Z3 via a NIX-shell config, so not sure we want to get into trying to override the Shell environment that NIX creates for us.

[rod-chapman]

How would your --external-solver-binary interact with the selection of the SMT back-end? The SMTLib generated for Z3 is very different from that generated for Bitwuzla, for example. How would I say "Here's an external solver binary, but please generate SMTLib as if it's Z3 please..." or similar? Not sure I like this option...

Would I need multiple scripts i.e. "z3_4.12.6_with_special_switches_1", "bitwuzla_latest_with_special_switches_2" etc. etc.?