apigen.py generates c errorCheck after solver_dec_ref()
#348
Assignees
Comments
|
Does #353 close this to our satisfaction, or something else needs to be done here? |
|
Oh, I overlooked this one :-( No, I do not think 353 solves it. I'll have a look first thing on Monday. |
janvrany
added a commit
to janvrany/MachineArithmetic
that referenced
this issue
Oct 21, 2024
Some Z3 APIs don't clear error (like some dec_refs and possibly others), so it could happen that, after encounting error (and reporting it) we call another Z3 functions which does not clear it and subsequent `#errorCheck` would report an error again (see [1]). An obvious solution - not to call `#errorCheck` for those API - is bit fragile - Z3 API is not explicit about which do and which don't and this is known to change version to version. So instead, we took the approach of clearing the error - this way each (detected) error is reported only once. [1]: shingarov#348
shingarov
pushed a commit
that referenced
this issue
Oct 21, 2024
Some Z3 APIs don't clear error (like some dec_refs and possibly others), so it could happen that, after encounting error (and reporting it) we call another Z3 functions which does not clear it and subsequent `#errorCheck` would report an error again (see [1]). An obvious solution - not to call `#errorCheck` for those API - is bit fragile - Z3 API is not explicit about which do and which don't and this is known to change version to version. So instead, we took the approach of clearing the error - this way each (detected) error is reported only once. [1]: #348
shingarov
pushed a commit
that referenced
this issue
Oct 28, 2024
Some Z3 APIs don't clear error (like some dec_refs and possibly others), so it could happen that, after encounting error (and reporting it) we call another Z3 functions which does not clear it and subsequent `#errorCheck` would report an error again (see [1]). An obvious solution - not to call `#errorCheck` for those API - is bit fragile - Z3 API is not explicit about which do and which don't and this is known to change version to version. So instead, we took the approach of clearing the error - this way each (detected) error is reported only once. [1]: #348
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
For every Z3 API call,
apigen.pygenerates aZ3_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: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.The text was updated successfully, but these errors were encountered: