Attention Boogie users,
Thanks to Sascha Böhme, Boogie now has support for real numbers. The syntax for integer division/modulus has changed and these operations are now interpreted. The rest of this message describes the full design (which Michal Moskal helped
design).
Rustan
 Add a new keyword, “real”. It denotes both a builtin type and an inttoreal conversion function.
 Add new keywords “div” and “mod”. They denote integer division and modulus.
 Syntax for real literals. Either of the following:
digit+ '.' digit+ ['e' [''] digit+ ]
digit+ 'e' [''] digit+
where superfluous leading zeros are okay. The base of the exponent is 10.
New operator overloadings:
 : real > real
+ : real * real > real
 : real * real > real
* : real * real > real
== : real * real > bool
!= : real * real > bool
< : real * real > bool
<= : real * real > bool
>= : real * real > bool
> : real * real > bool
New operators:
** : real * real > real Exponentiation
(which I think is not actually interpreted, but the intention is that it will be when the appropriate SMT support is there). This operator is rightassociative, and (despite what its width might suggest) it binds stronger than MulOp's in the grammar
(but weaker than unary operators).
div : int * int > int (Euclidean division, see
http://en.wikipedia.org/wiki/Modulo_operation)
mod : int * int > int (Euclidean modulus)
Changed operators:
/ : int * int > real
/ : int * real > real
/ : real * int > real
/ : real * real > real
Operators no longer supported:
%
New builtin functions:
int : real > int
real : int > real
