How to get different unsat kernels when using z3 using QF_LRA logic

Question

I use z3 to retrieve an unsaturated core of an unsatisfactory set of linear constraints. I find that z3 can give another unsaturated kernel for the same problem if the "auto-config" parameter is false. Are there other options that can cause z3 to give another unstable kernel for the same problem?

Here is my previous question related to us: How to get several different incompatible kernels or reduce the size of the kernel

Answer 1

There is no specific API for retrieving various unsatisfactory kernels, but you can use the existing API to retrieve some or all of the minimum kernels. Next tutorial

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

simplified illustrates how to get several kernels (or all) and several maximum satisfying sets (or all) at the same time.