test_cbmc_options="-DFORCE_FAILURE"