[PATCH] D54978: Move the SMT API to LLVM

Brian Rzycki via Phabricator via llvm-commits llvm-commits at lists.llvm.org
Wed Feb 13 11:39:00 PST 2019

brzycki added a comment.

In D54978#1395562 <https://reviews.llvm.org/D54978#1395562>, @mikhail.ramalho wrote:

> Hi @brzycki, but isn't it exactly what we want? I mean, if we try to cross-compile and it fails for any reason (non-native library, wrong version), then Z3_FOUND shouldn't be set.

I'm not sure, cross-compilation is tricky to get right.

> I just finished a small patch that checks the version as a run-time property. Please, let me know your thoughts.
>  If you agree with this approach I'll create a separate revision for it (it seems to work on ubuntu and fedora for me).

I'd be interested in seeing it and I'll happily provide feedback. I'm not sure if this method is better or worse than regex parsing of headers that @ddcc suggested.

No matter what algorithm chosen I'd strongly prefer the case when we are unable to ascertain the correct `Z3_VERSION_STRING` we should conservatively set this to `"0.0.0"` with a warning to inform the users early on something is strange with the version of Z3 being tested.

  rC Clang



More information about the llvm-commits mailing list