CODEWITHSUNDEEP
z3
Dingbao Xie
Dingbao Xie

Reputation: 736

How to get different unsat cores when using z3 on logic QF_LRA

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

Upvotes: 3

Views: 322

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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.

Upvotes: 4

Related Questions