[PPL-devel] Widening when CP0 is not included in CP1

[Mario Mendez]

Hi,

In the documentation you always remark the precondition CP0<=CP1 
required by widening(CP1,CP0). What is the usual strategy when the 
condition is not met? I mean, imagine a list of consecutive abstract 
values (1D polyhedrons) like
	{1<x<2}, {2<x<3},{3<x<4}, ....,{n<x<n+1}
How can we ensure converge in these cases?

Thanks!


Mario Mendez