[SMT-LIB] consider inclusion of exponentiation in FixedSizeBitVectors

Florian Schanda florian.schanda at altran.com
Wed Apr 5 03:48:47 EDT 2017


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.


More information about the SMT-LIB mailing list