Bugfix. The prior revision sometimes returned the wrong result (very rarely).
In the prior revision I removed some explicit calls to simplifyTerm.
Wrongly believing that the term was already simplified at the point.
To check that it was simplified I asserted the "hasBeenSimplified" function.
But the hasBeenSimplified function only checked that the term was present in the simplifyMap.
That is that simplifyTerm had been called on it.
Which isn't the same thing as being simplified.
i.e. term A is not simplified if in the SimplifyMap it's mapped to term B.
It's only simplified if A maps to A.
Some simplification functions expect their children to already be simplified.
This wasn't the case so we'd get the wrong answer.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@965
e59a4935-1847-0410-ae03-
e826735625c1