An agent writing its own library to interface with a good solver like Z3 (or even writing some basic planning algorithms itself) seems like the epitome of a "costly long term investment that does nothing for the short term". The only thing I can see overcoming such problems are deep search trees, but AFAIK that is not how LLMs work at all.