Unroll first and last iteration in encoding

[JonasAlaif]

For a

while(cond)
 invariant invs
{
  body
}

loops we can instead generate the CFG of essentially

if(cond) {
  do
   invariant invs
  {
    inhale cond
    body
  } while(cond)
}

This essentially unrolls the first and last loop iteration when executed in Silicon.
This change should be identical to viperproject/carbon#399 ⁠— i.e. we should add a flag for enabling this behavior.

The one thing I'm not sure about is the hardcoded Inhale(cond), sometimes we might want this to be an Assume? Is there any significant difference?