(error "Cannot handle general quantifiers in predicates at the moment")

[leonardoalt]

Sample: https://gist.github.com/leonardoalt/0e9d9bb399f80820f0e8025f27c2e2dd Command: eld -horn -t:10 a.smt2.

I'm not sure what exactly the error is referring to, the only quantifiers I use are foralls in the definitions of the rules. Any hints about what's wrong here?

[pruemmer]

I will have a look. The error message tells that interpolation was not able to compute quantifier-free predicates; this must be because of arrays in the clauses. Our CEGAR engine is sometimes not able to continue in such a case.

[pruemmer]

After some optimization of the ADT handling in the latest version, this example now seems to work!

[leonardoalt]

Nice! I tested the nightly on another example and get the same message, so just wanted to post on the existing issue: https://gist.github.com/leonardoalt/be507afe15506ca630707e2058122239