Domanda

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

Thanks.

È stato utile?

Soluzione

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

Autorizzato sotto: CC-BY-SA insieme a attribuzione
Non affiliato a StackOverflow
scroll top