Method unsat_core

lean_py/z3/solver.py:608–612

Return unsat core (not supported).

(self)

        self._assertions.append(a)

    def unsat_core(self) -> list:
        """Return unsat core (not supported)."""
        raise NotImplementedError(
            "Unsat core not supported: Lean is a proof checker, not an SMT solver"
        )

    def reason_unknown(self) -> str:
        """Return reason for unknown result."""