4

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.

pad
  • 41,040
  • 7
  • 92
  • 166
user1388672
  • 147
  • 1
  • 1
  • 9

1 Answers1

4

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

Community
  • 1
  • 1
Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53