Sireum has been adapted byt Zhi, example work once de-workaround.

Still: recursive procedures are not correctly generated by sireum.
Added a test file for the demo at Adacore (2014, nov 5th).