In the incremental smt2 decision procedure the array_exprt should be handled before being dispatched to the convert_expr_to_smt.
However in the failing test array_exprt expression are forwarded to the convert_expr_to_smt causing an invariant violation.

The test failing this is:

• cbmc/array-cell-sensitivity12/test_execution.desc