Z3 Optimize: add `assert_and_track` and `get_unsat_core`

prove-rs / z3.rs

Rust bindings for the Z3 solver.

337 stars 105 forks source link

Closed toolCHAINZ closed 2 months ago

toolCHAINZ commented 2 months ago

I noticed these are missing from Optimize and would have some use for them.

toolCHAINZ commented 2 months ago

Looks good to me apart from the comment… would it be easy to add a test for this?

Ok, I've added a test that exercises both assert_and_track + check and an individual check.

waywardmonkeys commented 2 months ago

Ok, I've added a test that exercises both assert_and_track + check and an individual check.

Great, thanks!