Re: SPARK and integer arithmetic

[Paul Rubin <no.email@nospam.invalid>]

Florian Weimer <fw@deneb.enyo.de> writes:
>>> perhaps there is a way to express the unbounded arithmetic ...
> The actual formula in the program uses modular arithmetic, so I don't
> think this can be represented efficiently in Presburger arithmetic.

Oh I didn't understand, I saw the modular arithmetic in your post but
thought you wanted to change it to unbounded arithmetic.  Still though,
if the modulus is a known constant, then a=b(mod m) means a+mx=b+my for
some x and y, and multiplication by the constant m can be converted to
repeated additions with depth log2(m).  So it's still in Presburger
arithmetic, with even that seeming like overkill.