smtlib parser: :named annotations lead to warnings

[quicquid]

Please consider the following smtlib script:

(set-info :smt-lib-version 2.6)
(set-logic UFNIA)
(set-option :produce-unsat-cores true)
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)

(assert (! (>= x 3) :named mx1 ))
(assert (! (<= x 3) :named mx2 ))
(assert (! (>= y 2) :named my1 ))
(assert (! (<= y 2) :named my2 ))
(assert (! (>= z 1) :named mz1 ))
(assert (! (<= z 1) :named mz2 ))

(assert
         (or
          (> 3 x)
          (>= y 3)
          (>= y x)
          (>= 0 (+ z y))
          )
 )
(check-sat)
(get-unsat-core)
(exit)

Each of the named assertion leads to a warning:

Warning Error while type-checking an attribute:
While typing: :named Unbound identifier: ':named'

I'm not sure how to interpret the warning - cvc4 and z3 correctly compute the unsat core for the problem though.

[Gbury]

Right, currently, I don't think that any smtlib annotations are recognized by the type-checker. I'll add support for the :named annotation, and the :pattern one (which I just found out while re-reading the smtlib spec), but are there other standards annotations for smtlib ?

[Gbury]

Sorry for the delay, this should be fixed in b4caf0b18a975b3581826975ddee594f3a2281ab