search

uuverifiers / eldarica

The Eldarica model checker
Other
81 stars 23 forks source link

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

Closed leonardoalt closed 3 months ago

leonardoalt commented 3 years ago

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 3 years ago

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 3 years ago

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

leonardoalt commented 3 years ago

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