Supporting R16, and fixing a bug with shortest counterexample for safety algorithm.