Hi club,
I updated my Why3 from 0.87.3 to 0.88.0 today and had a few issues with my
existing theories. I got some unbound symbol 'BVC.to_uint_small' errors
where BVC is an alias for bv.BVConverter_8_64. I suspect this to be due to
the new quote character syntax in identifiers. I have the same issu
On 15/10/2017 20:47, Julien Cretin wrote:
> Hi club,
>
> I updated my Why3 from 0.87.3 to 0.88.0 today and had a few issues with
> my existing theories. I got some unbound symbol 'BVC.to_uint_small'
> errors where BVC is an alias for bv.BVConverter_8_64. I suspect this to
> be due to the new quote
Hi,
Le 15/10/2017 à 20:47, Julien Cretin a écrit :
> Hi club,
>
> I updated my Why3 from 0.87.3 to 0.88.0 today and had a few issues with
> my existing theories. I got some unbound symbol 'BVC.to_uint_small'
> errors where BVC is an alias for bv.BVConverter_8_64. I suspect this to
> be due to th
Thanks Claude and Guillaume for your answers! I could solve my current
issue with your help.
And thanks also for the article about how to combine bit-vectors and
integers. It will help me come up with useful assertions (full bit-vector
expressions for drivers with bit-vector support) to avoid this
