Hi the following trace shows a soundness bug in Z3 with annotations. If I read the standard correctly the assert should be semantically equal to false.

[919] % z3 small.smt2
sat
[920] % cvc4 -q small.smt2
unsat
[921] % cat small.smt2
(assert (! false :lblpos +))
(check-sat)
[922] %

OS: Ubuntu 18.04
Commit: fdabaa6