Estou ciente de que a teoria dos inteiros com multiplicação é genericamente indecidível. No entanto, em certos casos, o Z3 retorna um modelo. Estou curioso para saber como isso é feito. Tem algo a ver com o novo procedimento de decisão para aritmética não linear sobre reais? Quais instâncias específicas (por exemplo: Integers sob módulo finito, etc.) foram reconhecidas para as quais Z3 retorna um modelo para uma consulta de multiplicação? Qualquer ajuda é muito apreciada.