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

Fabian Wolff fabi.wolff at arcor.de
Sun Oct 6 18:43:49 BST 2019


Hi Roman,

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

thanks for pointing this out to me.

4.8.6 is ready and uploaded, but because it introduced the new python3-z3 package,
it's still hanging in the NEW queue, which seems to be moving quite slowly recently:

  https://ftp-master.debian.org/new/z3_4.8.6-1.html

Unfortunately, all I can do at this point is to wait for someone from the FTP team
to review and, hopefully, accept the package, but I do not know when this is going
to happen (the package has been in the queue for about a week now).

Best regards,
Fabian



More information about the Pkg-llvm-team mailing list