Evaluación de una fórmula lógica a muchos valores en Z3.

Necesitaba evaluar el valor de una expresión sobre varios valores de variables usando Z3. Sé que Z3 es un verificador de satisfacción, pero model.Eval (Args) provoca evaluaciones de una expresión en los valores de las variables generadas por el modelo.

Entonces, ¿es posible para nosotros iterar sobre varios valores para evaluar una expresión?

Ejemplo: p y q en todos los valores posibles de p y q (p, q es booleano)

Entonces, en cierto sentido, crear una tabla de verdad a partir de ella usando alguna recursión o iteración. ¿Es posible de alguna manera que Z3 lo haga?

La ayuda con la API de C # será aún mejor.

Gracias