Yices2 Parser Problems

[baierd]

Yices2 supports parsing on our currently main branch. But the tests are still disabled for it and it fails many basic tests. This should be investigated and solved before the next release, or the parser should be removed until it is.

[baierd]

Here is an example of how Yices2 parses string input with the API call we currently use (yices_parse_term()). It looks like it is expecting formulas exclusively in its own format, no SMTLIB2 input. But it can parse SMTLIB2 with its executable, so it most likely has the capabilities.

There is a smt_parser.c file, and a yices_smt.c with the following documentation: Solver for problems in the SMT-LIB notation.

We should ask the developers for an API extension.