assertNoUnderflow1.v