How to get different unsat cores when using z3 on

问题:

I am using z3 to extract the unsat core of an unsatisfiable linear constraint set. I find z3 may give a different unsat core for the same problem when setting the "auto-config" option to false. Does there exist other options which may make z3 give a different unsat core for the same problem?

Here is my previous related question: How to get multiple different unsat cores or make the core smaller

回答1:

There is no specific API for getting different unsatisfiable cores, but you can use the existing API to retrieve some or all minimal cores. The following tutorial

http://rise4fun.com/Z3Py/tutorial/musmss

illustrates in a simplified way how to retrieve multiple cores (or all) and multiple maximal satisfying sets (or all) at the same time.