search

shingarov / MachineArithmetic

A mathematical foundation for Smalltalk-25
MIT License
17 stars 6 forks source link

`apigen.py` generates `c errorCheck` after `solver_dec_ref()` #348

Open shingarov opened 1 month ago

shingarov commented 1 month ago

For every Z3 API call, apigen.py generates a Z3_get_error_code(ctx) check right after the call. However, I just learned the hard way that not every Z3 API touches the error code. For example, solver_dec_ref() doesn't. In particular, it doesn't even reset it. So this:

| solver |
solver := Z3Solver new.
[ …some failing Z3 call… ] on: Z3Error do: [ ].
solver release.

will die inside Z3Solver>>release because it will think solver_dec_ref() failed when if fact it just didn't clean up the leftover error code.

shingarov commented 3 weeks ago

Does #353 close this to our satisfaction, or something else needs to be done here?

janvrany commented 3 weeks ago

Oh, I overlooked this one :-(

No, I do not think 353 solves it. I'll have a look first thing on Monday.