[SMT-LIB] consider inclusion of exponentiation in FixedSizeBitVectors

[Levent Erkok]

I'd be happy to contribute a few as well. It'd be great if a solver
supported it first (say CVC4), so I can be sure to produce a benchmark that
was at least syntactically correct.

-Levent.

On Wed, Apr 5, 2017 at 2:01 PM, Yannick Moy <moy at adacore.com> wrote:

> -- Clark Barrett (2017-04-05)
>
> This seems like a reasonable suggestion.  If we add it, would any of you
> be willing/able to provide a set of benchmarks using the new operator?
>
>
> I will certainly be willing to send you VCs generated from SPARK that use
> the new operator, once we've modified our generation to use it.
> Best regards
> --
> Yannick Moy, Senior Software Engineer, AdaCore
>
>
>
>