search

uuverifiers / eldarica

The Eldarica model checker
Other
80 stars 22 forks source link

Plans for theory combination? #33

Closed leonardoalt closed 3 years ago

leonardoalt commented 3 years ago

Hi there :) I just tried Eldarica on one of my benchmarks and got

Theories: ADT(tx_type), ADT(bytes_tuple), SimpleArray(1)
(error "Combination of theories is not supported")

Are there any plans to support that? Here's the smt2 file if anyone is interested: https://gist.github.com/leonardoalt/d797eca839f14bb1997de7c5a6496a83

pruemmer commented 3 years ago

Hi Leonardo,

yes, we are working on a new array solver that will be able to handle this combination as well. Should have something running by the next CHC-COMP ;-)

Best wishes, Philipp

leonardoalt commented 3 years ago

That's great! Thanks @pruemmer

pruemmer commented 3 years ago

The last master should now support this combination (arrays + ADTs), although the functionality is not much tested yet.

leonardoalt commented 3 years ago

@pruemmer awesome! I just tried it on the sample I posted earlier and it works perfectly. I'll try it on the rest of my benchmarks next week.