search

prove-rs / z3.rs

Rust bindings for the Z3 solver.
347 stars 110 forks source link

z3 optimize soft_assert weights can be negative #187

Closed aquarial closed 2 years ago

aquarial commented 2 years ago

Closes https://github.com/prove-rs/z3.rs/issues/186

The docs have been updated to show that negative weights are rewards: https://github.com/Z3Prover/z3/blob/master/src/api/z3_optimization.h#L85

sameer commented 2 years ago

Thanks for fixing this and correcting the documentation, Karl!