Re: SPARK and integer arithmetic

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

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.