Pergunta

Are there any other available (and still supported) SMT tools that perform quantifier elimination for linear integer arithmetic besides Z3?

Thanks.

Foi útil?

Solução

You can try Princess, by Philipp Rümmer. It supports quantifier-elimination and is actively maintained.

Licenciado em: CC-BY-SA com atribuição
Não afiliado a StackOverflow
scroll top