Etiqueta en afirmaciones SMT-LIB 2.0 en Z3

Question

¿Podría decirme cómo nombrar las afirmaciones en un punto de referencia Z3 SMT-LIB 2.0? Preferiría usar la sintaxis estándar de SMT-LIB, pero como Z3 parece no entenderlo, solo estoy buscando una que trabaje con Z3. La necesidad es obtener núcleos SASTS con etiquetas.

Aquí hay un ejemplo de punto de referencia que probé:

(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)

Espero el núcleo ASSAN {Hyp4, Hyp5} debido a la contradicción (x <y y y <= x), pero Z3 retomina:

(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
()

Entiendo que Z3 no entiende esta forma de nombrar, pero no pude encontrar otra forma en la documentación Z3.

¿Usted me podría ayudar por favor?

Answer 1

Si cambio tu primer comando de

(set-option enable-cores)

a

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

y que luego ejecuto tu script:

z3 -smt2 script.smt2

Obtengo como salida

unsat
(hyp4 hyp5)

Lo cual es que creo lo que esperabas. Tenga en cuenta que estoy usando Z3 3.2 (para Linux, pero eso no debería hacer ninguna diferencia).