I have a reasonably simple MILP (mixed integer linear program): https://0bin.net/paste/B1IE5l8l#2YLLrptC-l1ml+vesA59tH3167IOCAkJoIUQWbrj/mN
which I can solve with cbc optimally on my low-end computer in about 6.75 seconds.
I have tried to convert it to a format that z3 can take, making a few simplifications along the way and have this: https://0bin.net/paste/M5dDXNl2#-A3hnStDDZABP69+yBsCdEz818pif15r88SxD8qRwjX
but after half an hour I had to kill it without a solution.
Is there some trick I'm missing, or is z3 bad at solving these sort of MILPs?