Exception thrown by Solver.consequences()

[fsomenzi]

The attached code, with z3 4.13.3 runs for almost a minute and then throws

File "/usr/local/lib/python3.12/dist-packages/z3/z3.py", line 7262, in consequences
    r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.12/dist-packages/z3/z3core.py", line 4287, in Z3_solver_get_consequences
    _elems.Check(a0)
  File "/usr/local/lib/python3.12/dist-packages/z3/z3core.py", line 1566, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'Overflow encountered when expanding vector'

Similar examples run in almost no time, whether or not the assertions are satisfiable. This problem is not a show stopper for me because it only occurs in a buggy version of the program from which the attached example is extracted, but I thought you'd like to know.
standalone.zip