Dear Enea I would appreciate it to the more if you could shed some light on the following problem. Given the logic program p(0, X, X) :- !. p(N, X, Y) :- X1 is 0.75*X+1, N1 is N - 1, p(N1, X1, Y). such that recurses $N$ times over the expression $0.75*X+1$, find a fixpoint by which no overflow in the $X$ and $Y$ arguments can be proved. My proceeding on this includes the construction of two polyhedra: one for the base case; the other for the inductive case. Then I (try to) calculate the fixpoint using the program below. But a series of problem arise. For instance, for the inductive constraints as shown below (note in particular $B =< 10000$), the following abnormal halting error pops up, at the second fixpoint iteration: ERROR: Unhandled exception: 'Integer_to_integer_term()' Another constraints setting that produces the same error consists in removing $A <= 100$ and $B =< 10000$, and querying the program with ?- w(100). I would be thankful if you could suggest some hints on how to get a fixpoint for the program above. It might be that I do not declare enough constraints so that sufficient information to assure convergence is included. Many Thanks. Ciao, Javier ---------------------- In this program, argument $K$ corresponds to the bounds for triggering a widening operator (in this case the standard: H79). verbosity(1). w(K) :- make_vars(6, [A, B, C, D, E, F]), % Base case ppl_new_Polyhedron_from_dimension(c, 3, Base), ppl_Polyhedron_add_constraints(Base, [A = 0, B >= 0, C = B]), display_poly(['Base'],Base), % Inductive case ppl_new_Polyhedron_from_dimension(c, 6, Induc), ppl_Polyhedron_add_constraints(Induc, [A =< 100, A >= 0, B >= 0, B =< 10000, C >= 0, D >= A - 1, 4*E >= 3*B + 4, C = F]), display_poly(['Inductive'],Induc), % Previous polyhedron ppl_new_Polyhedron_empty_from_dimension(c, 3, Previous), fixpoint(1, K, Induc, Previous, Base, Fixpoint, N), display_poly(['Fixpoint'],Fixpoint), display_message(['reached in',N,'iterations']). %%%%%%%%%%%%%%%%%%%%%%%%%%% % Post-fixpoint calculation % Base case fixpoint(N, _, _, Previous, Current, Fixpoint, N) :- ppl_Polyhedron_contains_Polyhedron(Previous, Current), !, ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Fixpoint). % Inductive case fixpoint(N, K, Induc, Previous, Current, Fixpoint, M) :- make_vars(6, [A, B, C, D, E, F]), ppl_delete_Polyhedron(Previous), ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Previous1), ppl_delete_Polyhedron(Current), ppl_new_Polyhedron_from_Polyhedron(c, Induc, c, Current1), ppl_new_Polyhedron_from_dimension(c, 3, Aux), ppl_Polyhedron_concatenate_assign(Aux, Previous1), ppl_Polyhedron_intersection_assign(Current1, Aux), ppl_delete_Polyhedron(Aux), ppl_Polyhedron_remove_dimensions(Current1,[D,F,E]), ppl_Polyhedron_poly_hull_assign_and_minimize( Current1, Previous1), (N >= K, ppl_Polyhedron_H79_widening_assign(Current1, Previous1); true), display_poly(['Iteration ', N],Current1), N1 is N+1, fixpoint(N1, K, Induc, Previous1, Current1, Fixpoint, M). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % make_var_list(+I,+Dimension,?VariableList) % constructs a list of variables with indices from I to Dimension - 1. % It is assumed that I =< Dimension. make_vars(Dim, VarList):- make_var_list(0, Dim, VarList). make_var_list(Dim,Dim,[]):- !. make_var_list(I,Dim,['$VAR'(I)|VarList]):- I1 is I + 1, make_var_list(I1,Dim,VarList). %%%%%%%%%%%%%%%%%% % Output messages. display_poly(Message, Polyhedron) :- ppl_Polyhedron_get_constraints(Polyhedron, Constraints), display_message(Message), display_message(Constraints). display_message(Message):- verbosity(1), !, nl, write_all(Message), nl. display_message(_). write_all([]). write_all([Phrase|Phrases]):- write(Phrase), write(' '), write_all(Phrases).