[jeffffff]

this sounds like a case where no amount of unit testing ever would've found the bug. someone found the bug either through reasoning about the implementation or using formal methods and then wrote a test to demonstrate it. you could spend your entire life writing unit tests for this function and chances are you would never find out there was an issue. i'd say this is more of an argument for formal methods than it is for any approach to testing.

[Beldin]

But once you've found the bug, you'd like to add a test case that prevents regression - a test case that doesn't require a supercomputer.

That might not always be possible - but if it is, the test would be based on implementation details.