I'm always happy to have someone else upload a fix, just go ahead and do it. But in this case, the latest upstream no longer manifests the problem. Since there was no fix to the div.cpp test case, I suspect it was an actual bug that the test case picked up and upstream fixed. But I have not bothered to check.
Will close this big momentarily. --Barak.
