Procurando código-fonte Z3, me deparei com um monte de arquivos referentes a QF_FPA, que parece representar uma aritmética de ponto flutuante livre de quantificadores. No entanto, parece que não consigo localizar qualquer documentação sobre o seu estado, ou como ele pode ser usado através de vários front-ends (em particular o SMT-Lib2). Esta é uma codificação do IEEE-754 FP? Em caso afirmativo, quais precisões / operações são suportadas? Qualquer documentação seria mais útil ..