Could you tell me how to name the statements in the z3 SMT-LIB 2.0 test? I would rather use the standard SMT-LIB syntax, but since z3 doesn't seem to understand it, I'm just looking for work with z3. The need is to get unsaturated cores with tags.
Here is an example of the test 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 expect unsat core {hyp4, hyp5} due to a 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 have not found another way in the z3 documentation.
could you help me?
source
share