Macro z3_solve_u32 

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