Hello community,
I’m a Clang Static Analyzer developer and hereby I propose bumping the minimal Z3 requirement from 4.7.1 to 4.8.9.
I’m motivated by features that are only available from that version and upward: setting rlimit, for a deterministic threshold limiting time spent in Z3 queries.
You can read more about the use-case, I’m using this option here.
Given that Z3 is part of the llvm support library, I’m reaching out for having a discussion about bumping this version requirement.
However, I’m not aware of any users of the Z3 solver API other than the Clang Static Analyzer itself - where it’s an optional component.
I’m not aware of any buildbots testing with Z3, so I don’t think there is work w.r.t. build bots.
Given all, this I don’t think there is a major downside of raising the minimal Z3 version requirement. Let me know if I should proceed with the bump.
Thanks!
1 Like
It seems like this topic did not record much traction - which what I expected TBH.
I interpret this as that there is no objection for implementing this RFC.
I’ll wait for the llvm-weekly to get even wider visibility, and only implement this on Tuesday if still nobody objects.
I see that 4.8.9 was released in 2020. I think that should be old enough that people should be able to pick it up on most OSes/distros. I am OK with this change.
I’ve only recently encountered this topic from the already merged patch (unfortunately, I get like 1000 emails just from LLVM’s GitHub activity daily…).
Nota bene, the latest available version of libz3-dev on Ubuntu 20.04 LTS (the oldest still officially supported Ubuntu distribution) is 4.8.7. This might cause some problems, depending on how easy it is to otherwise obtain a working Z3 developer build of a different version.
(It’s just to keep in mind, I’m not suggesting we should quickly downgrade the requirement to allow .7 instead of .9.)