Fix detecting refinement of trace (State needs to be backtracked not only when its method call stack contains a refined method, but when it is reached by executing the method somewhere on the way). Some further comments