Commit 58ece73 introduced pool Z3FuncDeclKind. (Integer) values of
those "decl kinds" were taken from Z3 4.13.0.
However, it turned out that Z3 commit 9fa00aec1 1 introduced new
kind - Z3_OP_RECURSIVE - that did not exist before. Unfortunately it
was done in a way that that the integer value is the same as what
USED TO BE value of Z3_OP_UNINTERPRETED and Z3_OP_UNINTERPRETED got
assigned new value
This means that the value of Z3_OP_UNINTERPRETED differ, depending on
version. This commit works around the problem by updating value depending
on actual Z3 version at runtime.
An obvious place to do so would be in pool initialize but that does
not work for two reasons:
(i) initialize is called at the time package is loaded, meaning
before user have a chance to specify which library to use
(LibZ3 class >> libraryName:). So it may or may not update to
correct values. Worse, it may bind to the wrong library too early,
making LibZ3 class >> libraryName: useless.
(ii) for the same reason, if something goes wrong it'd difficult to
debug.
So instead, this code updates values just before the very first context
is create and/or when image is restarted.
shingarov
commented
3 months ago
Commit
58ece73introduced poolZ3FuncDeclKind. (Integer) values of those "decl kinds" were taken from Z3 4.13.0.However, it turned out that Z3 commit 9fa00aec1 1 introduced new kind - Z3_OP_RECURSIVE - that did not exist before. Unfortunately it was done in a way that that the integer value is the same as what USED TO BE value of
Z3_OP_UNINTERPRETEDandZ3_OP_UNINTERPRETEDgot assigned new valueThis means that the value of
Z3_OP_UNINTERPRETEDdiffer, depending on version. This commit works around the problem by updating value depending on actual Z3 version at runtime.An obvious place to do so would be in pool
initializebut that does not work for two reasons:(i) initialize is called at the time package is loaded, meaning before user have a chance to specify which library to use (
LibZ3 class >> libraryName:). So it may or may not update to correct values. Worse, it may bind to the wrong library too early, makingLibZ3 class >> libraryName:useless. (ii) for the same reason, if something goes wrong it'd difficult to debug.So instead, this code updates values just before the very first context is create and/or when image is restarted.