FS#64460 - Do not force -DUSE_LIB_GMP=1 for configuring Z3.
Attached to Project:
Community Packages
Opened by Daniel Kirchner (ekpyron) - Monday, 11 November 2019, 17:50 GMT
Last edited by Felix Yan (felixonmars) - Monday, 07 September 2020, 20:57 GMT
Opened by Daniel Kirchner (ekpyron) - Monday, 11 November 2019, 17:50 GMT
Last edited by Felix Yan (felixonmars) - Monday, 07 September 2020, 20:57 GMT
|
Details
The Z3 PKGBUILD explicitly sets "-DUSE_LIB_GMP=1". The
default is *not* to link against GMP.
Why is that? I'm asking because we recently stumbled upon cases, in which Z3 could solve a problem, if *not* linked against GMP, while it failed to solve it, when linked against GMP. There might, of course, be cases with the opposite behavior, but my question is: what's the reason for not keeping it at the upstream default? |
This task depends upon
Closed by Felix Yan (felixonmars)
Monday, 07 September 2020, 20:57 GMT
Reason for closing: Implemented
Additional comments about closing: 4.8.8-2
Monday, 07 September 2020, 20:57 GMT
Reason for closing: Implemented
Additional comments about closing: 4.8.8-2
I'll wait for an answer from upstream on the issue you mentioned: https://github.com/Z3Prover/z3/issues/2551#issuecomment-552536486
I don't think z3 has any open bugs because of the non GMP implementation. I also think it would make sense to not use GMP in this package (same as upstream).