I don't have the 1978 paper by Cousot & Halbwachs at hand. However, if I interpret correctly what you write, P-true is the entry condition to the true branch and P-false is the entry condition to the false branch. So up to here we all agree.
Where we disagree is that your annotations p1 and p2 still have the constraint `j = 0', which is wrong. I don't know what you are doing. What you should do is, I believe, to compute p1 as the affine image of P-true with respect to j = i+2 and p2 as the affine image of P-false with respect to j = i. These images would not have the constraints `j = 0' that you have.
To summarize, here is what you should have and what I obtain with the PPL:
*** P_true *** j = 0, i >= 0. *** P_false *** j = 0, -i > 0. *** After P_true.affine_image(j, i+2), call this p1 *** i - j = -2, j >= 2. *** After P_false.affine_image(j, i), call this p2 *** i - j = 0, -i > 0. *** After p1.poly_hull_assign_and_minimize(p2) *** i - j >= -2, -i + j >= 0.
Please, let us know if this clarifies things enough. Ciao,
Roberto
Ok, I found the error. When I have a linear non invertible assign (like j:=i+2) I call 'ph.add_constraint(j == i+2)' in order to insert a new constraint (I don't remember because I have done it. Problably I though that an assignment introduced always a new constraint to my polyhedra). I use 'affine_image' for linear invertible assign only (for ex: i:=i+2).
Thanks Roberto, your help is more and more useful.
Enrico.