Specify explicit theory in SMT solver backend

[yav]

There might be performance benefits if we explicitly tell the solver what theories to use.

[dc-mak]

We should also add Z3 flags to adjust performance like this: Z3Prover/z3#7352

[cp526]

As of 0ef1e70 CN specifies the logic in the CVC5 backend. It would be easy to add a Z3 setting for the flag mentioned above.