1
votes

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

Thanks.

1

1 Answers

1
votes

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