Question

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

Thanks.

Était-ce utile?

La solution

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

Licencié sous: CC-BY-SA avec attribution
Non affilié à StackOverflow
scroll top