[SMT-LIB] consider inclusion of exponentiation in FixedSizeBitVectors

[Yannick Moy]

Hi,

Is it planned to include exponentiation in FixedSizeBitVectors theory? Currently, we're using an uninterpreted function with an axiomatization for it, which leads to poor performance (typically all such goals end up not being proved). It seems that provers that support FixedSizeBitVectors natively could also support exponentiation.

Best regards
--
Yannick Moy, Senior Software Engineer, AdaCore