Relationship between minimize/maximize and assert_soft

[LeventErkok]

If a problem contains both a minimize (or a maximize) of an arithmetic goal, and also calls to assert-soft, how do these interact?

Will z3 "optimize" and ignore if the optimized arithmetic value violates the soft-assertions? Or will it try to satisfy the soft-assertions first, and then optimize the arithmetic goal for the maximally satisfiable soft-assertion set?

Related: How do the weights play a role on this. (I don't see a way to attach a weight to a maximize/minimize goal though.)

I've looked through the optimization paper (https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf) but I didn't see anything specific regarding this aspect.

Thanks!