# Z3 solver