Add support for UNSAT core to the OpenSMT backend#375

Merged

kfriedberger merged 14 commits into

add-unsat-core-opensmt

May 19, 2024

Commits on May 2, 2024

OpenSMT: Updated to the latest OpenSMT version.
daniel-raffler
committed
OpenSMT: Added support for unsat core. Note that this feature is new and marked as 'experimental' in OpenSMT.
daniel-raffler
committed
OpenSMT: Added missing checks in getUnsatCore.
daniel-raffler
committed
OpenSMT: Enable unsat core tests for OpenSMT.
daniel-raffler
committed
OpenSMT: Make sure that models are only created when ProverOptions.GENERATE_MODELS was acutally selected.
daniel-raffler
committed
OpenSMT: Set logic to QF_LIA in unsat core tests as OpenSMT lacks support for unsat core in its more general logics.
daniel-raffler
committed
OpenSMT: Disable tests for unsat core that require assumptions.
daniel-raffler
committed
OpenSMT: Added a native API test for unsat core.
daniel-raffler
committed
OpenSMT: Fixed a bug in the JNI bindings for MainSolver.getUnsatCore()
daniel-raffler
committed

Commits on May 8, 2024

Commits on May 19, 2024