Support SMT solvers other than z3

[Boyan-MILANOV]

We should support other solvers backends.
Being able to export constraints in the SMTlib v2 format would also be really nice.

• Export constraints to smtlibv2
• Yices
• Boolector
• CVC5
• Others ? See https://smt-comp.github.io/2022/results.html