search

uuverifiers / eldarica

The Eldarica model checker
Other
80 stars 22 forks source link

question about Unrecoverable Syntax Error #41

Closed izlatkin closed 2 years ago

izlatkin commented 3 years ago

Hello,

Does eldarica support only some particular smt-lib formates / has partially support?

For example, it returns "Unrecoverable Syntax Error" for every smt2 files generated by https://github.com/seahorn/seahorn or for the majority of the files from https://github.com/grigoryfedyukovich/aeval/tree/student-projects/bench_horn

Are declare-rel, declare-var supported?

thank you

pruemmer commented 3 years ago

Eldarica currently only supports standard SMT-LIB input. The operations declare-rel, declare-var are a Z3 extension for their fixedpoint engine, and not part of the standard language.

You can use the chc-tools to convert between those different formats: https://github.com/chc-comp/chc-tools

izlatkin commented 3 years ago

How exactly I can do this? It is not really clear from readme how to launch the tool.

pruemmer commented 3 years ago

I cannot comment on this unfortunately. You will need to download and compile the tool first, but concerning the use of the tool it is best if you create as issue in the chc-tools repository!