Re: SPARK and integer arithmetic

[Florian Weimer <fw@deneb.enyo.de>]

* Paul Rubin:

> Florian Weimer <fw@deneb.enyo.de> writes:
>> The intent is that I can write unbounded integer arithmetic in
>> predicates and post-conditions.
>> Not too surprisingly, gnatprove can't deal with this (I've already
>> been told it's beyond alt-ergo, and Z3 can only brute-force it).  But
>> perhaps there is a way to express the unbounded arithmetic so that
>> there is less work left for the prover?
>
> I think there is some way for Spark to use Coq, which can deal with
> things like that easily.  The Wikipedia article on Presburger arithmetic
> also cites http://ieeexplore.ieee.org/document/6987606/?arnumber=6987606
> about using (adapting?) the CVC4 SMT solver on quantifier-free
> arithmetic expressions.

The actual formula in the program uses modular arithmetic, so I don't
think this can be represented efficiently in Presburger arithmetic.
Or am I missing something?