Empty unsatCore for simple contradictions in assumptions

[CaelmBleidd]

If we have a simple contradiction (e.g., 2 > 3 or false) in constraints passed into io.ksmt.solver.KSolver#checkWithAssumptions function, for Z3 we've got an empty unsat core. Looks like it is a problem with Z3 API that returns empty cores for such simple situations, but as a result, we don't have information about contradicting assertions in the solver.

Example to reproduce:

    @Test
    fun testUnsatCore(): Unit = with(context) {
        context = KContext()
        z3Solver = KZ3Solver(context)
        yicesSolver = KYicesSolver(context)

        val z3Status = z3Solver.checkWithAssumptions(listOf(mkFalse()))
        val z3UnsatCore = z3Solver.unsatCore()

        val yicesStatus = yicesSolver.checkWithAssumptions(listOf(mkFalse()))
        val yicesUnsatCore = yicesSolver.unsatCore()

        println(z3Status to z3UnsatCore)
        println(yicesStatus to yicesUnsatCore)
    }