search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
332 stars 62 forks source link

Reworking Windows patch mechanism #35

Closed aytey closed 5 years ago

aytey commented 5 years ago

Reworking the Windows patch mechanism to not be dependant upon a specific revision. Patches are now applied against any revision, as long as they apply cleanly. Otherwise, compliation does not continue.

Signed-off-by: Andrew V. Jones andrew.jones@vector.com

aytey commented 5 years ago

Updated with Windows patches for the latest CaDiCaL

aytey commented 5 years ago

Given the issues with 32-bit Windows and CaDiCaL, I am just reworking the Windows patches to restore mobical (right now, this patch set disables its compilation, but it can actually be made to work).

mpreiner commented 5 years ago

Ok, should I wait with merging until this is fixed?

aytey commented 5 years ago

Yep, won't be long (< 30 minutes).

aytey commented 5 years ago

Okay, all done.

With this updated patch-set for CaDiCaL, CaDiCaL now builds correctly on 32-bit and passes a (subset) of the CaDiCaL test-suite.

make test inside of the CaDiCaL build will run the usage, cnf and trace tests (it does not run api or mbt) -- running just these first three were enough to find an issue on 32-bit Windows.

mpreiner commented 5 years ago

@andrewvaughanj Thanks for all the work!