Baier D.

I've tested the prebuilt `dll` and it does not load and i don't know why. I will investigate further.

Update: The precompiled binary needs 3 additional dependencies: `libwinpthread-1.dll`, `libstdc++-6.dll` and `libgcc_s_seh-1.dll`. I tried simply statically link these, but there are 2 problems and i could only solve one. The...

I don't know if that is possible for Windows. The Yices2 devs only provide build documentation for Cygwin + Mingw (and Cygwin alone). I can test it and take a...

I tested building the Yices2 version on Linux, however the config does not seem to work for that purpose. I might need to ask the Yices2 devs for help here...

@kfriedberger Yices2 is not thread safe by default and we need a re-entrant version if we want to use it multithreaded. Yices 2 supports multithreading on seperate contextes only (so...

Since i had difficulties running Yices2 in re-entrant mode (unpredictable behavior; SAT/UNSAT on the same problem when running multiple times etc.) i tried several compiliation changes and contacted the devs....

Current state: - There is (at least) 1 test that fails on slower systems (CI) sometimes. - Yices2 is still problematic. (But since development of Yices2 seems stale at the...

Since the problem with the tests described above seems to be only a timeout when initializing threads, it was easily fixable by increasing the timeout time. @kfriedberger would you add...

CVC5 currently does not provide API for formula translation between distinct solver contexts, but they are working on a solution for that. Further, CVC5 does not provide a termination callback...

Greetings @lorenzleutgeb, the implementation is done except for the interpolation prover. We are currently communicating with the CVC5 devs about some problems there. We just need to upload the binary...