Macro z3_solve_u16 

z3_solve_u16!() { /* proc-macro */ }