Add support to Z3

[celinval]

Requested feature: Add Z3 as a Kani solver option
Use case: As we investigate adding support to quantifiers, using SMT solvers will increase the quantifier expressiveness.
Link to relevant documentation (Rust reference, Nomicon, RFC):

Note: Z3 should be enable in CBMC with: --incremental-smt2-solver "z3 --smt2 -in"

[celinval]

I created this commit to enable it (celinval@f87c387), but we still need to assess how much support these two solvers have once we upgrade to CBMC 6.0. I tried it with the 5.9 version, but it is pretty broken due to unsupported goto constructs.