Exception thrown by Solver.consequences() #7443
Description
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