When I told them about it they said that the -rcheck code was inherited from MiniSAT. Since it's also not enabled by default it's understandable that it hadn't

When I told them about it they said that the -rcheck code was inherited from MiniSAT. Since it's also not enabled by default it's understandable that it hadn't been as thoroughly checked as usual. I wouldn't blame them if they just dump it instead of fixing it. But yes it is strange that it doesn't verify its outputs. On the other hand SAT solvers want to be as fast as possible and there shouldn't be a need to do it if the solver is operating correctly.