CIF data-based synthesis currently has the following code, a special-case termination check for the controllability reachability computation: ```java if (fixedPointComputation == CTRL && cifBddSpec.settings.getTermination().isRequested()) { if (dbgEnabled) { cifBddSpec.settings.getDebugOutput().dec(); } return; } ``` I'm not sure why this is only for one of the fixed-point computations, and for all of them. Maybe it is a leftover from when the different reachability computations were generalized and put into a loop, so that each was executed using similar code, I'm not sure. In any regard, I think it should do the termination check for all of them.