[Z3] Fix Z3FuncDeclKind for Z3 <= 4.8.15

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.

[1]: Z3Prover/z3@c9fa00aec1

Author: janvrany

src/Z3/Z3Context.class.st

@@ -26,8 +26,19 @@ Z3Context class >> current [
 
 { #category : #'instance creation' }
 Z3Context class >> from: aZ3Config [
-	^Z3 mk_context: aZ3Config 
+	"Create and return new Z3Context"
 
+	"And now something horrible. We need to update (some or)
+	 Z3FuncDeclKind values, depending on a version. Rather than
+	 doing it at class initialization time, we do it lazily,
+	 just before first context is created and/or when image
+	 is restarted. This makes it easier to debug when something
+	 goes wrong. Sigh."
+
+	(Global isNil or:[ Global isNull ]) ifTrue:[
+		Z3FuncDeclKind update.
+	].
+	^Z3 mk_context: aZ3Config
 ]
 
 { #category : #'instance creation' }

src/Z3/Z3FuncDeclKind.class.st

@@ -586,7 +586,39 @@ Z3FuncDeclKind class >> initialize02 [
 	Z3_OP_FPA_BVWRAP := 45098 .
 	Z3_OP_FPA_BV2RM := 45099 .
 	Z3_OP_INTERNAL := 45100 .
-	Z3_OP_RECURSIVE := 45101 .
-	Z3_OP_UNINTERPRETED := 45102 .
+	Z3_OP_RECURSIVE := 'Z3FuncDeclKind class >> #update not called' copy.
+	Z3_OP_UNINTERPRETED := 'Z3FuncDeclKind class >> #update not called' copy.
+]
+
+{ #category : #private }
+Z3FuncDeclKind class >> update [
+	"Update enum values depending on version of Z3 we're
+	 using - ugly indeed."
+
+	| ver |
+
+	ver := Z3 getVersion.
+
+	"Z3 commit c9fa00aec1 introduced new kind - Z3_OP_RECURSIVE.
+	 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, making this
+	 change not compatible. Therefore, here we check the version
+	 and try to update pool values accordingly. Sigh.
 
+	[1]: https://github.com/Z3Prover/z3/commit/c9fa00aec1
+	"
+	(ver first > 4 or: [ ver second > 8 or: [ver third > 15 ]]) ifTrue: [
+		"Z3 > 4.8.15"
+		Z3_OP_RECURSIVE := 45101 .
+		Z3_OP_UNINTERPRETED := 45102 .
+	] ifFalse: [
+		"Z3 <= 4.8.15"
+		Z3_OP_RECURSIVE := 'Not defined for Z3 <= 4.8.15' copy.
+		Z3_OP_UNINTERPRETED := 45101 .
+	].
+
+	"
+	Z3FuncDeclKind update
+	"
 ]