Optimizer weights can be negative

[aquarial]

https://github.com/prove-rs/z3.rs/blob/master/z3/src/optimize.rs#L240 ensures weights are positive:

let weight_valid: bool = *self >= 0;
assert!(weight_valid, "Weight cannot be negative");

This is consistent with the API: https://github.com/Z3Prover/z3/blob/master/src/api/z3_optimization.h#L85

However Z3 accepts and properly handles negative weights. Z3py does not assert if the weight is positive: https://z3prover.github.io/api/html/z3py_8py_source.html#l07833

I've also opened an issue with the documentation at https://github.com/Z3Prover/z3/issues/5876 as well