Does Z3 give the minimal unsatisfiable core up to now?
I want to know if Z3 now can give the minimal unsatisfiable core now. Or is there someone has developed a good support for this? Does anybody know this?
Thank you very much.
Z3 produces unsatisfiable cores, but they are not necessarily minimal.
Here is an example on how to extract unsat cores: http://rise4fun.com/Z3/smtc_core
You may also want to check the following questions: