In my project I've been practicing a similar loop as you describe: an agent writes code, SMT solver checks against a spec. A few things I observed:

1. Solver is great at the bugs tests miss (overflow, off-by-one, empty inputs...), its output can be used by the agent to fix it.

2. Solver struggles where you'd assume: loops, non-linear arithmetic and pointer aliasing blow up solve time, floating point is painful.

So your step 2 would cover some of it well, but since the game code is a lot of floating point, SMT would probably have a hard time (get stuck/timeout).