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.

Answers


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:

Soft/Hard constraints in Z3

Label on SMT-LIB 2.0 assertions in z3


Need Your Help