CiaoPP: termination analysis and compositionality

[simonefulvio-rollini]

Hello,

I am trying termination analysis on the following example:

:- module(test19, [p1/2], [assertions,nativeprops]).

:- entry p1(X, Z) : (num(X), var(Z)).
:- check comp p1(X, Z) : (num(X), var(Z)) + terminates.

p1(X, Z) :-
    p2(Y),
    Z is Y + X.

:- trust pred p2(X) : var(X) => int(X) + terminates.
:- impl_defined(p2/1).

Apparently, the tool cannot prove that p1 terminates:

{WARNING (ctchecks_pred_messages): (lns 5-5) Could not verify assertion:
:- check comp p1(X,Z)
   : ( num(X), var(Z) )
   + terminates.
because
    terminates
could not be derived from inferred comp:
[shfr]         ground([X,Z]) 
[eterms]       num(X),num(Z) 
[nfdet]        [native_props:nondet([X,Z]),native_props:covered([X,Z]),native_props:mut_exclusive([X,Z])] 
[generic_comp] [No info available]
}

Can you please help me understand if I am missing something? Do I have to enable some preprocessor option?

Thanks,
Simone