[This description extraced from an email sent to Andrei
Voronkov. Remarks in [] added where context may be missing].

> Is there any logical description of the bug? How does is come out??

Yes, there is. You may have seen the new contracting inference rule
Simplify-Reflect in my talk [at CADE-16, the paper is in the
proceedings] (well, it was new to me, but it is pretty obvious, so it
may have been around before) [if it was, it apparently has not been
widely published]:


s=t   u[sigma(s)]!=u[sigma(t)] v L1...Ln
---------------------------------------- 
           L1....Ln  

The rule is not very strong, but its fairly cheap to implement - you
only need to check unorientable unit equations s=t (otherwise it is
subsumed by rewriting), you most often only need to check it at the
top level (if the top symbols differ), and you can use pdt-indexing,
which is implemented in E anyways. [pdt = perfect discrimination tree]

Of course, you can also allow a whole set of equations and allow more
differences in the removed literal. In this case, you have to use
recursion or a stack to implement the rule. However, for the case of
single equation s=t, as in the version above, (which covers most cases
anyways), you can descent into the term linearly.

Consider the case

f(t1...ti...tn) != f(t1...ti'...tn) 
  
If I want to apply the rule, I'll either have to find an equation that
connects ti and ti' in a single step, or else ti and ti' have to have   
the same top symbol and I have to check their corresponding subterms.
 
Now conside the case

f(t1...ti...tj...tn) != f(t1...ti'...tj'...tn)

where ti and ti' can be connected. I recorded this success and
traversed the remaining arguments. On hitting the second difference,  
the correct thing is to terminate unsuccessfully - I terminated with
the success status of the previous check, i.e. I forgot to reset the
success bit (in the code, that amounted to a misplaced break
statement, leaving an inner loop but forgetting about the outer one).

The mininal example I came up with that triggers the bug is on the E
website:
# Test file for simplify-reflect. If your prover proves this, it is
# buggy. If it runs for more than a couple of seconds it is slow or
# uses a calculus that cannot deal well with equality. If it
# terminates with a "no proof found" message, it is (perhaps) fine.
#
#          

g(X)=g(Y).
f(g(a),a)!=f(g(b),b).

The recommended option -u for old versions of E selects the stronger,
multi-equation version of simplify-reflect, and hence circumvents the
bug.