Some boogie programs do not parse

[delcypher]

I found 3 programs in this repository that do not parse

First

ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c_.bpl does not parse due to use of a reserved type name (real) as a variable name

procedure dm_tm_create_non_blocking_clone(real: int)

Second

ldv-consumption/linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c_.bpl does not parse for the same reason as the above boogie program

Third

ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--gpu--drm--via--via.ko-entry_point_true-unreach-call.cil.out.c_.bpl does not parse due to the use of a reserved keyword (then, used in if-then-else expressions) as a variable name.

procedure time_diff(now: int, then: int)

I suspect this was a bug in SMACK when these boogie programs were created but I do not have a working copy of SMACK to test if this is still a bug.