[MrJohz]

But how do you do PBT here without having a known-correct algorithm available? Because that scenario is seldom the case in practice.