Now that the ModelChecker and NodeStack have been refactored a bit, I don't
need to rely on create_cv() to avoid overwriting a previously-existing
clockvector; create_cv() will now be called at most once per ModelAction. So
change this condition to an ASSERT().