Multiway Decision Graphs (MDGs) have been recently proposed as an efficient verification tool for RTL designs based on an efficient representation mechanisms. In MDG, a data value is represented by a single variable of abstract sort, and a data operation is represented by an uninterpreted function symbol. In this work we investigate the non-termination problem of MDG-based verification. We present a novel approach to dealing with the problem based on retiming and circuit transformations that preserve the behavior of the circuit. We demonstrate the effectiveness of our method on the example of the Island Tunnel Controller (ITC).