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.
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.