- Implement smt and smt-z3/smt-cvc4 as options for --solvers

- Uses a main solver sources for verification/CLP, taking into account
  --solvers

- Implement Z3-SMT sets

- Add tests for Z3-SMT