z3-solver>=4.12.2
