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.

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