Support check-sat-using tactic for Z3

[PhilippWendler]

Z3 provides not only check-sat but also check-sat-using <tactic> in SMTLib, so probably also via the API. This can be used to let Z3 use different solving strategies, which might be more effective in some scenarios.

Users would like to experiment with this (example), so I suggest we add a configuration option for Z3 that lets users specify such a tactic which then gets used for all solving calls.