Quality of Unsatisfiable Cores

Nov 3, 2013 at 7:51 PM
Running z3 on this smt2 instance,

(set-option :produce-unsat-cores true)
(set-logic QF_LIA)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)
(declare-fun x5 () Int)
(assert (! (<= x1 0) :named s_0))
(assert (! (<= x2 0) :named s_1))
(assert (! (<= x3 0) :named s_2))
(assert (! (<= x4 0) :named s_3))
(assert (! (<= x5 0) :named s_4))
(assert (<= 1 (+ x1 x2 x3 x4 x5)))
(check-sat)
(get-unsat-core)

gives the following answer:

unsat
(s_4 s_3 s_2 s_0 s_1)

Although the answer is correct i would expect
a higher quality unsatisfiable core (any pair
of the assumptions).

Is there any option or something to be modified
to get a better core.

Thanks.