Eu estou usando z3 para extrair o núcleo unsatfiable de um conjunto de restrições lineares insatisfeita. Acho z3 pode dar um núcleo diferente unsat para o mesmo problema ao definir a opção "auto-config" para false. Existem outras opções que podem fazer com que o z3 ofereça um diferente núcleo insaturado para o mesmo problema?

Aqui está a minha pergunta relacionada anterior:Como obter vários núcleos insaturados diferentes ou tornar o núcleo menor