Satisfiability Modulo Theories, SMT, solvers are used inmany applications. These applications benefit from thepower of tuned and scalable theorem proving technologiesfor supported logics and specialized theory solvers.SMT solvers are primarily used to determine whether formulas are satisfiable.Furthermore, when formulas are satisfiable, many applications need modelsthat assign values to free variables.Yet, in many cases arbitrary assignments are insufficient,and what is really needed is an <i>optimal</i> assignmentwith respect to objective functions. So far, users of Z3,an SMT solver from Microsoft Research, build custom loopsto achieve objective values. This is no longer necessarywith νZ (new-Z, or max-Z), an extension within Z3 that letsusers formulate objective functions directly with Z3. Under the hood there is aportfolio of approaches for solving linear optimization problems overSMT formulas, MaxSMT, and their combinations. Objective functions are combinedas either Pareto fronts, lexicographically, or each objective is optimized independently.