Both EXE and DART will never terminate if a loop condition is symbolic and unconstrained. What is the "right" way to deal with this limitation? Motivate your solution with theoretical and/or practical reasons.