Is there a way in Z3 to output the subset of clauses which forms the unsat core given an unsatisfiable conjuction of clauses? In my case input formula is a conjunction of atomic formulas in QF_AUFBV.
It would be really great if someone can help me with my query.
Thanks,
Sagar