Allow configuring the choice of SMT solver

Currently, `copilot-verifier` hard-codes the use of Z3, but in principle, it should be able to support any SMT solver. We should offer a verifier option to configure the SMT solver based on the choices that Copilot offers [here](https://github.com/Copilot-Language/copilot/blob/71dd87048a26d458fef8eb4fd6d318d6a497ea48/copilot-theorem/src/Copilot/Theorem/What4.hs#L85).
