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 #348).
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.
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
#errorCheckwould report an error again (see #348).An obvious solution - not to call
#errorCheckfor 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.