Bruno Dutertre

@yuanyuan1024. Apologies for the website problem. We're trying to get it fixed. In case this helps, you can generate the doc for Yices yourself. You need to install the Sphinx...

More exactly: The Yices API does not export the exists-forall solver, so it's not directly available in the Python API either. But, you can implement an exists/forall solver using the...

This is not documented but LIA is supported (but it's not heavily tested). Feel free to try.

This is all true. Converting yices internal terms to the SMT-LIB syntax is not trivial and we don't have that yet. I just wanted to record an issue so that...

Try to compile statically and in debug mode. For example: ``` make static-check MODE=debug ``` will run all the tests with assertions enabled.

Static builds work fine for me on x86_64 (and have for a long time). No special flag required. The main issue is building GMP in PIC mode.

The three versions is only for windows. On other platforms, you can build GMP once in PIC mode. You'll have libgmp.a for linking statically and libgmp.dylib for linking dynamically.

This was an optimization but it now looks like a mistake. Not many people use unit types anyway so I'm not sure the speedup is that important. It would be...

Make sure it works for people who don't use brew.