[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via llvm-commits]

mikhail.ramalho added a comment.

In D54978#1395561 <https://reviews.llvm.org/D54978#1395561>, @brzycki wrote:

> In D54978#1395476 <https://reviews.llvm.org/D54978#1395476>, @mikhail.ramalho wrote:
>
> > I'm wondering if we can remove the binary requirement all together: is it possible to run a small program that would return EXIT_SUCCESS if the library is the correct version?
>
>
> Hi @mikhail.ramalho, I don't think this is feasible unfortunately. If we're using a cross-compiler the emitted binary won't be native to the platform. In other words, you cannot test for Z3 as a run-time property.


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 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).


Repository:
  rC Clang

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

https://reviews.llvm.org/D54978