ksmt-core/io.ksmt.solver/KSolver/unsatCore

unsatCore

abstract fun unsatCore(): List<KExpr<KBoolSort>>

Retrieve the unsat core for the last check or checkWithAssumptions.

Unsat core consists only of:

  1. assumptions provided in checkWithAssumptions

  2. expressions asserted with assertAndTrack