If a block contract is surrounded by a construct with a termination spec, the block should implicitly get a termination contract (presumably the one from the function spec). Currently the following verifies:

void test()
_(decreases 0)
{

_(ensures \true)
{
    while (1) {}
}

}