Hi, for the following formula,
z3 9398601

(declare-fun y () Int)
(declare-fun c () (Seq Int))
(declare-fun b () (Seq Int))
(assert (forall ((x Int)) (and (= (seq.nth c y) (seq.nth c 0)) (not (= (seq.nth c x) (seq.nth b x))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 594
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

NB: strings are not supported in the new core yet.
This hits some debug code that performs evaluation with respect to strings (sequences) being interpreted and starts complaining. It is not too useful to look for bugs with unsupported interpreted theories because the debug check is not as permissive to consider this.

--
(thanks for the explanation!