search

prove-rs / z3.rs

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

Fix smt based tests #236

Closed Pat-Lafon closed 1 year ago

Pat-Lafon commented 1 year ago

In playing around with enabling the error_handler, I noticed that the tests for #226 were actually incorrect but there was no error checking so this was just ignored.(Whoops, my bad)

Maybe the api should be changed to avoid this? Something akin to https://github.com/prove-rs/z3.rs/blob/691ac9782f361969e87ac745a3d9a6816593741a/z3/src/tactic.rs#L207-L211. In general, I think there should be a better story for integrating with Z3's errors.

waywardmonkeys commented 1 year ago

Agree that we should do something better about the error integration!