throw error when synchronous (doesn't work if in callback)
fix for priorities in Z3
allow multiple default solvers, just make sure that identity solver is
unique for now