So far, Z3 gives the minimum unjustified core?

Question

I want to know if Z3 can now give a minimal intangible core. Or is there someone who has good support? Does anyone know this?

Many thanks.

+3

user1388672 May 11 '12 at 5:52

1 answer

Leonardo de moura · Answer 1 · 2012-05-11T17:35:34+0000

Z3 creates unsatisfactory cores, but they are not necessarily minimal.

Here is an example of how to retrieve unsat core: http://rise4fun.com/Z3/smtc_core

You can also check the following questions: