Bug#941857: Z3 4.8.4 contains cache bugs and should not be packaged

[Roman Lebedev]

Package: z3
Version: 4.8.4-1
Severity: serious
Tags: patch

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Dear maintainer.
It is good to see Z3 4.8.4 finally being packaged in Debian!

As i have personally just encountered, that version contains some bugs,
that result in incorrect modelling, which effectively renders the whole
library unusable. Upstream developer, Nuno Lopes, notes:
> https://github.com/AliveToolkit/alive2/issues/122
> https://github.com/AliveToolkit/alive2/issues/123#issuecomment-538761842
> BTW, it's important to have a recent Z3 so you can get the counterexample
> above. I fixed a bug a while ago in Z3's model cache (I don't remember which
> release it integrated).

I have manually rebuilt z3-4.8.6 from salsa and `sudo dpkg -i` it.
That resolved the bugs i was observing.

I personally consider these bugs to be fatal to the package,
as in it would be better to unpackage said package version.
Given that 4.8.6 is ready to be packaged thanks to the work of
Fabian Wolff, it may be good to proceed with that.

Roman.

- -- System Information:
Debian Release: bullseye/sid
  APT prefers unstable
  APT policy: (990, 'unstable'), (500, 'unstable-debug'), (1, 'experimental-debug'), (1, 'experimental')
Architecture: amd64 (x86_64)

Kernel: Linux 5.2.0-3-amd64 (SMP w/8 CPU cores)
Locale: LANG=en_US.UTF-8, LC_CTYPE=en_US.UTF-8 (charmap=UTF-8), LANGUAGE=en_US (charmap=UTF-8)
Shell: /bin/sh linked to /usr/bin/dash
Init: systemd (via /run/systemd/system)

Versions of packages z3 depends on:
ii  libc6       2.29-2
ii  libgcc1     1:9.2.1-8
ii  libstdc++6  9.2.1-8

z3 recommends no packages.

z3 suggests no packages.

- -- no debconf information

-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEjkF6151RK40WXe2HCDw+u0oWieAFAl2aIgcACgkQCDw+u0oW
ieDzoA//XwAtgmtGsnsK6siLKlGmpnDw3kMrNVwNx7HgBAyBc87q/ag0OuoZ5HdY
iEi302NPH84dAcF8xLK0XgrPAMiBYHnm5AerRzVV7hiZ9x1nbBrW9Ueo4pItBZKv
vf38PQpXdiMf7oXyn9vaarmAJXpOM/aenfjqit+8gBz1c0UobdIDNhY2/ZZ3xEG7
Ca3xFzqVvIwCJRuGiFwqr1zlP1opvEkLaTZ2N77/9bkYArAs36vJfISSyUpMztLJ
6nvFNKhROLUrEVIQzr97QojjWC57PLVpiYkGuLriDKkCi5gSLcVLzgTevh2aNKkW
dEZCoWjEFyMRi1HXqorgBZSoOKqI850rAtx58EE9MA7eiu+rHrHSuezFSGYPKI8W
RQoMBMXiTBPDZ7cKG6QvQ2J3ITscwqE6Oc0w3VYpK57eGjdQ8hWCRJagdBpEyzTv
/xfJHOisTFMwz7SH179EuavnYvS2I0IWcHuS0/pHkra0P4cweaQ4tw0qrQhbdJsu
GEh98u6/qHO0A2vIi+0/Q5b1I5h6ViwDlipv7o57q60+hSqKzanzdchg3vg/A65S
MuoJM7WoD7OkxBUThiFgHSjJCjMGGhF/XWLLseKOmM7FHQgZVhmnEDZPgqKqnDnS
kGQsa0tpt6w1IJfvFUWpnZfUNLS119ncphLrW0h7tL7K2WfICHA=
=SmuQ
-----END PGP SIGNATURE-----