[SMT-LIB] consider inclusion of exponentiation in FixedSizeBitVectors

Yannick Moy moy at adacore.com
Wed Apr 5 01:04:38 EDT 2017


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





More information about the SMT-LIB mailing list