Sequences/map: Decidability regression

[LeventErkok]

For:

(set-logic ALL)
(declare-fun xs () (Seq Int))
(assert (= (seq.map (lambda ((x Int)) (+ 1 x)) xs)
           (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))))
(check-sat)
(get-model)

I'm currently getting (z3 built today):

unknown

But with z3 compiled on Feb 17 2023 (about 3 weeks ago), I was getting the correct answer:

sat
(
  (define-fun xs () (Seq Int)
    (seq.++ (seq.unit 0) (seq.unit 1) (seq.unit 2)))
)

I'm wondering if this is a regression in decidability; or one of those things that stays in the gray area and may or may not work depending on the z3 build.