prove-rs / z3.rs

Rust bindings for the Z3 solver.
337 stars 105 forks source link

Implement += for Solver #269

Closed Pat-Lafon closed 10 months ago

Pat-Lafon commented 10 months ago

The python bindings have solver += Bool which seems like some handy sugar.

I was also experimenting with overloading the operation with both &Bool and Bool which seems somewhat convenient but that isn't something I feel too strongly about.

Tested via a Doctest to raise awareness