Skip to content

Add support for unsat core to the OpenSMT backend #374

@daniel-raffler

Description

@daniel-raffler

Hello,
there has been some recent work on adding unsat core to OpenSMT (see here and here). Just as for interpolation the feature will be limited to formulas in QF_UF, QF_LIA or QF_LRA and support is still experimental at this point. Nevertheless we should consider updating our own bindings.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions