test_cbmc_options="-DASSERT_END"