[PPL-devel] Re: Fixpoint + Widening in PPL

[Enea Zaffanella]

Dear Javier,

J. Nunez Fontarnau wrote:
> Dear Enea
> 
> The purpose of constraints such as B =< 10000 is to bound the values of variable
> B according to the numemrical system underlying it, for instance, for an
> imaginary floating point system such that would permit the representation of
> values no greater than 10000. The case of A =< 100 has no justification: it was
> just a "what if ..." constraint. :)

reconsidering your program, it seems to me that you forgot to provide 
these "numerical system bounds" for variables B and C for the base case 
of your inductive computation. Namely,

   ppl_Polyhedron_add_constraints(Base, [A = 0, B >= 0, C = B])

is already allowing for an "overflowing computation", so there is no 
hope that the final result will be bounded. I guess you should, at the 
very least, add the constraint B =< 10000 also here.

Ciao,
Enea.