(error "Cannot handle general quantifiers in predicates at the moment")
leonardoalt opened this issue · 3 comments
leonardoalt commented
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 commented
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 commented
After some optimization of the ADT handling in the latest version, this example now seems to work!
leonardoalt commented
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