TLDR: It seems like the fix in #2460 has been reverted, and the bug has resurfaced again.

Array values in the Z3 model sometimes show up as lambda terms, but in Z3 Java API, they get represented as a Quantifier instead --- but Quantifier.getBody is no longer guaranteed to be a BoolExpr. Thus, if I call Quantifier.getBody on a lambda term, sometimes Java throws a cast error, and there is no good way to overcome this. In particular, it seems like the fix in the above issue has been reverted in the commit 3bca1fb

From a user point of view, it would be great if lambda values in the Z3 model actually get represented as a z3.Lambda AST node in the Java API (or alternatively, not have Quantifier be a subclass of BoolExpr) --- but at a minimum, it would be good if Quantifier.getBody can be fixed again to not perform a forced cast.