Looks like the bug has been fixed already. - Yang On 01/23/2018 09:56 PM, John Regehr wrote:
Pascal Cuoq reports this one: https://pastebin.com/D7aaZv5r John