[SMT-LIB] consider inclusion of exponentiation in FixedSizeBitVectors

[Florian Schanda]

On Wednesday 05 Apr 2017 07:04:38 Yannick Moy wrote:
> 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.

We've actually had support for this in Riposte, but it was fairly slow. 
Martin, can you remember how we did this?

But yeah, I'd like to +1 this, it would be good for SPARK 2014.