I wrote a CSP solver a while ago. The bugs were alarmingly prone to being incomplete enumeration of solutions. The solver would say "Yep, here's all 2412 solutions to that problem", but there were more solutions out there it missed. I didn't usually know how many solutions there would be so it's hard to distinguish between "all of them" and "95% of them". However that also threw a lot of doubt on when the solver returned unsat - was the problem unsat, or was the solver failing to look in part of the search space?
I didn't find a plausible testing strategy for convincing myself that the last of that class of error was gone and ultimately stopped working on it as a result.
I didn't find a plausible testing strategy for convincing myself that the last of that class of error was gone and ultimately stopped working on it as a result.