division by zero not modeled

[crhf]

It seems that some division by error are missed. For example, modInt is modeled as a boogie function, but the mod operation can actually throw when modulus is 0. Do I need to make modInt a procedure to model this?

[martinschaef]

Yes ... but again, Boogie probably changed since, so I don't know what their semantics is. But, in general, I would model functions if you want to control their behavior.