How to Determine the Solver and Options Used by Z3?

[rvandoren]

Hi,
I have a question regarding the solvers and default options used by Z3 when verifying SMT files. Is there an option or command in Z3 that outputs the solver type and default solver options being used?
For instance, if I specify "incremental" optimization parameter, does it automatically configure Z3 to use an incremental solver? Or, in this case, is it still necessary to explicitly add a push statement in the SMT file to enable incremental solving?
Thank you in advance!