Label on SMT-LIB 2.0 assertions in z3

Question

Could you tell me how to name assertions in a z3 SMT-LIB 2.0 benchmark? I would prefer to use the standard syntax of SMT-LIB, but as z3 seems not to understand it, I'm just looking for one working with z3. The need is to get unsat cores with labels.

Here is an example of benchmark I tested:

(set-option enable-cores)
(set-logic AUFLIA)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (! (<= 0 x) :named hyp1))
(assert (! (<= 0 y) :named hyp2))
(assert (! (<= 0 z) :named hyp3))
(assert (! (< x y) :named hyp4))
(assert (! (and (<= 0 y) (<= y x)) :named hyp5))
(assert (! (not (= x z)) :named goal))
(check-sat)
(get-unsat-core)

I am expecting the unsat core {hyp4, hyp5} because of the contradiction (x < y and y <= x), but z3 returns:

(error "ERROR: line 10 column 31: could not locate id  hyp1.")
(error "ERROR: line 11 column 31: could not locate id  hyp2.")
(error "ERROR: line 12 column 31: could not locate id  hyp3.")
(error "ERROR: line 13 column 30: could not locate id  hyp4.")
(error "ERROR: line 16 column 36: could not locate id  hyp5.")
(error "ERROR: line 18 column 35: could not locate id  goal.")
sat
()

I understand that z3 does not understand this way of naming, but I could not find another way in z3 documentation.

Could you help me please?

Answer 1

If I change your first command from

(set-option enable-cores)

to

(set-option :produce-unsat-cores true)

and that I then run your script:

z3 -smt2 script.smt2

I get as an output

unsat
(hyp4 hyp5)

which is I believe what you were expecting. Note that I'm using Z3 3.2 (for Linux, but that shouldn't make any difference).