feat request: add support for user-defined objectives like optimization

[0xalpharush]

Is your feature request related to a problem? Please describe.
For issues like rounding or trying to maximize the amount of an asset received, it would be nice to have an automated tool to exacerbate the rounding error or maximize the amount received.

Describe the solution you'd like
Create a mode to find minimums/maximums instead of checking for reachability of assertions. Z3 seems to have built-in support for this but it's inner workings or limitations are a mystery to me...

Describe alternatives you've considered
Using a fuzzer or effectively brute force search. It may be possible to repeatedly replace the value returned by Halmos and ask it for N+1 in a loop but I'd assume the SMT solvers have a better way to optimize than this

Additional context
https://microsoft.github.io/z3guide/docs/optimization/arithmeticaloptimization/

[karmacoma-eth]

We could give this a try, but I'm not convinced that it would work well, if at all. Do you have a motivating example we could try it on?