You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: