Likely GMP bug

[Hans Åberg]

> On 28 May 2018, at 11:34, Torbjörn Granlund <tg at gmplib.org> wrote:
> 
> "Marco Bodrato" <bodrato at mail.dm.unipi.it> writes:
> 
>  It was hard, but we got it:
>  https://gmplib.org/repo/gmp/rev/1f8a8fefb5c2
> 
> Thanks!
> 
> It really worries me that our crazy broad testing did not catch this
> until now.  This makes me much less confident about GMP's correctness,
> actually.

Full formal semantics verification would require something like Hoare logic.