Sorry, missed this one earlier.

When we register a relation, such as LE_EXPR,  we first check if there 
is an existing relation that applies, and if so they are combined. We 
were checking if the relation being registered was an EQ_EXPR, and if 
so, invoked the equivalence oracle.

  I was doing the check for EQ_EXPR first, then merging with any 
existing relation.   In this case, the merge resulted in transforming 
the LE_EXPR into an EQ_EXPR, but the check to invoke the 
equivalence_oracle had already been done, and we got to a place we 
shouldn't have. doh!

The fix is to do the merge first, then check for EQ_EXPR.

The patch is a hair different (due to VREL_*  renames in gcc13), so I've 
attached both patches.

bootstraps on gcc12 and gcc13 with no regressions.  pushed on trunk.

OK for GCC12?

Andrew