Eliminate excessive internal calls to "simplify"

[geo2a]

In attempt to reduce the number of expensive calls to Kore's simplifier, I've propagated the calls closer to the return points in Proxy.hs. We still also call simplifyExecuteState to detect vacuous results in the following cases:

• We've finished rewriting in Booster without falling back to Kore;
• We've finished rewriting in Kore, but did not make any steps, i.e. got Stuck or Branching.

Obviously, things will change dramatically after merging #389, but I think these changes still may be worth having on main, to make it so that we can remove the remaining "simplify" call with more confidence. the SMT integration has been merged.