1test_cbmc_options="-DFORCE_FAILURE"
2