search

GaloisInc / what4-solvers

Multi-platform binary creation for solvers of the versions most suitable for use with What4
5 stars 1 forks source link

Upgrade CVC5 version when fix for cvc5/cvc5#8900 is released #31

Closed RyanGlScott closed 1 year ago

RyanGlScott commented 1 year ago

Recently, CVC5 implements a fix for cvc5/cvc5#8900 that (1) is critical to making CVC5 work correctly with SBV on Windows (see LeventErkok/sbv#644), and (2) avoids an annoying issue where using CVC5 with SBV on macOS/Linux creates files named "stdout". Ideally, we could just backport the fix for cvc5/cvc5#8900 to the most recent CVC5 release (1.0.4 at the time of writing), but that would not help on Windows, where we currently have to rely on using a cross-compiled binary that we download from CVC5's website. See #4. As a result, we would either have to work around #4 and build our own cross-compiled CVC5 first (which sounds painful), or we would have to wait for a new CVC5 release. I'm inclined to do the latter.

RyanGlScott commented 1 year ago

Another reason to upgrade the CVC5 version is to bring in the changes from cvc5/cvc5#7512, which will make it possible to build CVC5 natively on Windows.