[PATCH] D54978: Move the SMT API to LLVM

Brian Rzycki via Phabricator via cfe-commits cfe-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.


Repository:
  rC Clang

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D54978/new/

https://reviews.llvm.org/D54978





More information about the cfe-commits mailing list