I would like to use redlog to perform symbolic quantification of formulas over bitvectors. The formulas I'm dealing with use normal arithmetic operations (+,-, and constant multiplication), bit-wise operations, and relational operators (=,<,>,...). All of this can in principle be encoded using Presburger arithmetics with congruence. For my application it is important that the resulting expression after quantification is as concise as possible (which is why I cannot use bit blasting). My preliminary experiments with Redlog look promising; however I noticed that the structure of the result depends on the encoding of the input formula.

Therefore I was wondering if the Redlog community has experience with this type of problems. Perhaps there are some publications or software that I could look at to get some ideas for efficient encoding of bitvectors?

Thanks!

Leonid