Estoy interesado en MAX-SAT y esperaba que Z3 tuviera esto como una función incorporada. ¿Hay planes para hacer esto en un futuro cercano?

En ausencia de lo anterior, he intentado usar la aplicación maxsat de ejemplo desde la línea de comandos. Desafortunadamente, siempre que hago exec.sh "filename.z3", siempre obtengo la siguiente respuesta: "verificando si las restricciones estrictas son satisfactorias ... resultado: 0". ¿Qué estoy haciendo mal? Le aseguro que esta respuesta parece ser bastante independiente del contenido real del archivo.

Finalmente, los comentarios en el ejemplo de maxsat no especifican claramente cómo marcar las restricciones como duras o suaves. Una restricción dura se supone que es una fórmula precedida por: fórmula, y una restricción suave una fórmula precedida por: suposición. Entonces, para marcar "(assert (> x 0))" como suave, ¿dónde exactamente colocamos el ": assumption"? (He leído la consulta sobre restricciones duras y blandas, pero la pregunta / respuesta parecía estar más en el contexto de encontrar núcleos insatisfiables, en lugar de "núcleos máximos satisfactorios" de fórmulas no satisfactorias).