(Z3Py )проверка всех решений уравнения

В Z3Py, как я могу проверить, имеет ли уравнение для заданных ограничений только одно решение?

Если более одного решения, как я могу их перечислить?