Abstract We look at composition of (possibly nonterminating) high-level programs over situation calculus action theories. Specififically the problem we look at is as follows: given a library of available ConGolog programs and a target program not in the library, verify whether the target program executions be realized by composing fragments of the executions of the available programs; and, if so, synthesize a controller that does the composition automatically. This kind of composition problems have been investigated in the CS and AI literature, but always assuming fifinite states settings. Here, instead, we investigate the issue in the context of infifinite domains that may go through an infifinite number of states as a result of actions. Obviously in this context the problem is undecidable. Nonetheless, by exploiting recent results in the AI literature, we devise a sound and well characterized technique to actually solve the problem