Cleanup ml prover 3

I have been able to track down the root cause that makes the merge sort example fails from time to time. However, it is a bit hard to fix it before cleaning up several important classes. This pull request is the first step towards this direction. It consists of many bug fixes and small refactorings. I also try to make the prover's behavior more deterministic so that the merge sort example fails less often.
right, this is the leftover of the automatic refactoring