Consider performing some preprocessing

[bclement-ocp]

QF_BV/uclid/catchconv/convert-jpg2gif-query-1213.smt2 is a fairly trivial problem. Even when replacing all bitvector functions with uninterpreted symbols, Z3 is able to solve it in hundreds of ms using the solve-eqs tactic, which (as far as I can tell) simply substitute equalities, which means that there must be an "obvious" contradiction somewhere.

On the other hand, Alt-Ergo takes more than 30s on the same problem, and there is definitely something we can do there. For one, we could aggressively substitute variables with their definition at least when the definition is either a variable or a constant. This would help with hash-consing.

[bclement-ocp]

Note that when everything is uninterpreted, we do solve much faster (2s).

Reintroducing ony bvadd as interpreted causes the issues to pop up again, so this is due to a difference in the way we treat (bvadd t u) and (int2bv (+ (bv2nat t) (bv2nat u))).