delcypher added a comment.

In D54978#1431788 <>, @ddcc wrote:

> The only relevant commit that I can find is 
>  , but it first landed in z3 4.6.0. It looks like it's specific to CMake 
> though, so is it different if you use the python build? I haven't tried the 
> CMake build.

Hmm this looks like there are some bugs in the different Z3 build systems.

So for the CMake build the value of `Z3_FULL_VERSION_STR` is used to populate 
the `Z3_FULL_VERSION` macro in the header file. Initially this is 
 but then
If the git has is available we append to it
and if the git description is available we append to it
This was my attempt at mimicking the `get_full_version_string()` function (
 ) when I added Z3's CMake build system.

Unfortunately this doesn't quite match what Z3's python build system does.

- In the python build system the `VER_REVISION` global (used to set 
`Z3_REVISION_NUMBER` macro and is the forth integer in `Z3_FULL_VERSION`, i.e. 
`d` in `a.b.c.d`)  tries to count the number of commits reachable from the 
current git `HEAD` (see
 ). The CMake build system doesn't mimic this. Personally I don't think the 
python build system makes sense here at all given that this integer goes in the 
4th position in the version output (i.e. `d` in `a.b.c.d`).

- In the CMake build system the 4th integer in `Z3_FULL_VERSION` is always 
whatever `Z3_VERSION_TWEAK` is set to in the root `CMakeLists.txt` file. So 
far, I think has always been `0`.

So the bug here is that the CMake and python build systems don't agree on the 
meaning of the 4th version field. Personally I think the implementation of Z3's 
CMake build system makes more sense given where it is placed in the version 
string but that means the name `Z3_REVISION_NUMBER` macro name isn't very 

None of this really mattered until the version header file became public

Would one of you be able to file a bug against Z3 to fix this? I am no longer 
in a position to contribute to Z3 so I can't do this.


cfe-commits mailing list

Reply via email to