Nice. So here we have two testcases that catch different bugs, and you can never prove the absence of bugs by adding more testcases. But testing still works well enough in practice that people rarely write fully formal proofs for software, or for math theorems for that matter :-)