test_cbmc_options="-DFORCE_FAILURE_3"