Estou interessado no MAX-SAT e esperava que o Z3 tivesse isso como um recurso embutido. Existe algum plano para fazer isso no futuro próximo?

Na ausência do acima, tentei usar o aplicativo maxsat de exemplo a partir da linha de comando. Infelizmente, sempre que exec.sh "filename.z3", sempre obtenho a seguinte resposta: "verificando se hard limitaints são satisfatíveis ... result: 0". O que estou fazendo de errado? Garanto-lhe que esta resposta parece ser bastante independente do conteúdo real do arquivo.

Por fim, os comentários no exemplo do maxsat não especificam claramente como marcar restrições como hard ou soft. Uma restrição rígida deve ser uma fórmula precedida por: formula e uma restrição soft uma fórmula precedida por: assumption. Então, para marcar "(assert (> x 0))" como soft, onde exatamente colocamos o ": assumption"? (Eu li a consulta sobre restrições hard e soft, mas a questão / resposta parecia estar mais no contexto de encontrar núcleos insatisfatórios, em oposição a "núcleos com máxima satisfação" de fórmulas insatisfeitas.)