~ ceval_and_ceval_step_coincide.
~ ceval_deterministic'.
~ no_whiles_terminating.