optimize_get_unsat_core method

Z3_ast_vector optimize_get_unsat_core(
  1. Z3_context c,
  2. Z3_optimize o
)

\brief Retrieve the unsat core for the last #Z3_optimize_check The unsat core is a subset of the assumptions \c a.

def_API('Z3_optimize_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))

Implementation

Z3_ast_vector optimize_get_unsat_core(
  Z3_context c,
  Z3_optimize o,
) {
  return _optimize_get_unsat_core(
    c,
    o,
  );
}