Added and briefly tested the updated syntax. NaN/oo not supported yet

9 files changed, 1213 insertions, 1126 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 9d37476f..1d35b735 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -695,10 +695,10 @@ namespace Microsoft.Boogie.AbstractInterpretation
           Lo = floor;
           Hi = ceiling;
         } else if (node.Val is BigFloat) {
-          BigNum floor, ceiling;
+          BigInteger floor, ceiling;
           ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling);
-          Lo = floor.ToBigInteger;
-          Hi = ceiling.ToBigInteger;
+          Lo = floor;
+          Hi = ceiling;
         } else if (node.Val is bool) {
           if ((bool)node.Val) {
             // true
diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index 3c4cc40a..5f711e70 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -1,475 +1,507 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-

-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Diagnostics.Contracts;

-using System.Diagnostics;

-

-namespace Microsoft.Basetypes

-{

-  using BIM = System.Numerics.BigInteger;

-    

-  /// <summary>

-  /// A representation of a 32-bit floating point value

-  /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit significand

-  /// </summary>

-  public struct BigFloat

-  {

-    //Please note that this code outline is copy-pasted from BigDec.cs

-

-    // the internal representation

-    [Rep]

-    internal readonly BigNum significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left)

-    [Rep]

-    internal readonly int significandSize;

-    [Rep]

-    internal readonly BigNum exponent; //The value of the exponent is always positive as per fp representation requirements

-    [Rep]

-    internal readonly int exponentSize; //The bit size of the exponent

-    [Rep]

-    internal readonly String value; //Only used with second syntax

-    [Rep]

-    internal readonly bool isNeg;

-

-    public BigNum Significand {

-      get {

-        return significand;

-      }

-    }

-

-    public BigNum Exponent {

-      get {

-        return exponent;

-      }

-    }

-

-    public int SignificandSize {

-      get {

-        return significandSize;

-      }

-    }

-

-    public int ExponentSize {

-      get {

-        return exponentSize;

-      }

-    }

-

-    public bool IsNegative {

-      get {

-        return this.isNeg;

-      }

-    }

-

-    public String Value {

-      get {

-        return value;

-      }

-    }

-

-    public static BigFloat ZERO(int exponentSize, int significandSize) { return new BigFloat(false, BigNum.ZERO, BigNum.ZERO, exponentSize, significandSize); } //Does not include negative zero

-

-    private static readonly BigNum two = new BigNum(2);

-    private static readonly BigNum one = new BigNum(1);

-    private static BigNum two_n(int n) {

-      BigNum toReturn = one;

-      for (int i = 0; i < n; i++)

-        toReturn = toReturn * two;

-      return toReturn;

-    }

-

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Constructors

-

-    //Please note that these constructors will be called throughout boogie

-    //For a complete summary of where this class has been added, simply view constructor references

-

-    [Pure]

-    public static BigFloat FromInt(int v) {

-      return new BigFloat(v.ToString(), 8, 24);

-    }

-

-    public static BigFloat FromInt(int v, int exponentSize, int significandSize)

-    {

-      return new BigFloat(v.ToString(), exponentSize, significandSize);

-    }

-

-    public static BigFloat FromBigInt(BIM v) {

-      return new BigFloat(v.ToString(), 8, 24);

-    }

-

-    public static BigFloat FromBigInt(BIM v, int exponentSize, int significandSize)

-    {

-      return new BigFloat(v.ToString(), exponentSize, significandSize);

-    }

-

-    public static BigFloat FromBigDec(BigDec v)

-    {

-      return new BigFloat(v.ToDecimalString(), 8, 24);

-    }

-

-    public static BigFloat FromBigDec(BigDec v, int exponentSize, int significandSize)

-    {

-      return new BigFloat(v.ToDecimalString(), exponentSize, significandSize);

-    }

-

-    [Pure]

-    public static BigFloat FromString(String v, int exp, int sig) { //String must be

-      return new BigFloat(v, exp, sig);

-    }

-

-    public BigFloat(bool sign, BigNum exponent, BigNum significand, int exponentSize, int significandSize) {

-      this.exponentSize = exponentSize;

-      this.exponent = exponent;

-      this.significand = significand;

-      this.significandSize = significandSize+1;

-      this.isNeg = sign;

-      this.value = "";

-    }

-

-    public BigFloat(String value, int exponentSize, int significandSize) {

-      this.exponentSize = exponentSize;

-      this.significandSize = significandSize;

-      this.exponent = BigNum.ZERO;

-      this.significand = BigNum.ZERO;

-      this.value = value;

-      this.isNeg = value[0] == '-';

-    }

-

-    private BigNum maxsignificand()

-    {

-      BigNum result = one;

-      for (int i = 0; i < significandSize; i++)

-        result = result * two;

-      return result - one;

-    }

-    private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; }

-

-

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Basic object operations

-

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]

-    public override bool Equals(object obj) {

-      if (obj == null)

-        return false;

-      if (!(obj is BigFloat))

-        return false;

-

-      return (this == (BigFloat)obj);

-    }

-

-    [Pure]

-    public override int GetHashCode() {

-      return significand.GetHashCode() * 13 + Exponent.GetHashCode();

-    }

-

-    [Pure]

-    public override string/*!*/ ToString() {

-      Contract.Ensures(Contract.Result<string>() != null);

-      return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;

-    }

-

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Conversion operations

-

-    /// <summary>

-    /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!

-    /// Converts the given decimal value (provided as a string) to the nearest floating point approximation

-    /// the returned fp assumes the given significand and exponent size

-    /// </summary>

-    /// <param name="value"></param>

-    /// <param name="significandSize"></param>

-    /// <param name="exponentSize"></param>

-    /// <returns></returns>

-    public static BigFloat Round(String value, int exponentSize, int significandSize)

-    {

-      int i = value.IndexOf('.');

-      if (i == -1)

-        return Round(BigNum.FromString(value), BigNum.ZERO, exponentSize, significandSize);

-      return Round(i == 0 ? BigNum.ZERO : BigNum.FromString(value.Substring(0, i)), BigNum.FromString(value.Substring(i + 1, value.Length - i - 1)), exponentSize, significandSize);

-    }

-

-    /// <summary>

-    /// NOTE:  THIS METHOD MAY NOT WORK AS EXPECTED!!!!

-    /// Converts value.dec_value to a the closest float approximation with the given significandSize, exponentSize

-    /// Returns the result of this calculation

-    /// </summary>

-    /// <param name="value"></param>

-    /// <param name="power"></param>

-    /// <param name="significandSize"></param>

-    /// <param name="exponentSize"></param>

-    /// <returns></returns>

-    public static BigFloat Round(BigNum value, BigNum dec_value, int exponentSize, int significandSize)

-    {

-      int exp = 0;

-      BigNum one = new BigNum(1);

-      BigNum ten = new BigNum(10);

-      BigNum dec_max = new BigNum(0); //represents the order of magnitude of dec_value for carrying during calculations

-

-      //First, determine the exponent

-      while (value > one) { //Divide by two, increment exponent by 1

-        if (!(value % two).IsZero) { //Add "1.0" to the decimal

-          dec_max = new BigNum(10);

-          while (dec_max < dec_value)

-            dec_max = dec_max * ten;

-          dec_value = dec_value + dec_max;

-        }

-        value = value / two;

-        if (!(dec_value % ten).IsZero)

-          dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division

-        dec_value = dec_value / two;

-        exp++;

-      }

-      if (value.IsZero && !dec_value.IsZero) {

-        dec_max = new BigNum(10);

-        while (dec_max < dec_value)

-          dec_max = dec_max * ten;

-        while (value.IsZero) {//Multiply by two, decrement exponent by 1

-          dec_value = dec_value * two;

-          if (dec_value >= dec_max) {

-            dec_value = dec_value - dec_max;

-            value = value + one;

-          }

-          exp--;

-        }

-      }

-

-      //Second, calculate the significand

-      value = new BigNum(0); //remove implicit bit

-      dec_max = new BigNum(10);

-      while (dec_max < dec_value)

-        dec_max = dec_max * ten;

-      for (int i = significandSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the significand is fully calculated

-        dec_value = dec_value * two;

-        if (dec_value >= dec_max) {

-          dec_value = dec_value - dec_max;

-          value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation

-        }

-      }

-

-      return new BigFloat(false, BigNum.ZERO, BigNum.FromString(value.ToString()), exponentSize, significandSize); //Sign not actually checked...

-    }

-

-    // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).

-    /// <summary>

-    /// NOTE:  THIS PROBABLY WON'T GIVE USEFUL OUTPUT!!!

-    /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative

-    /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.

-    /// </summary>

-    /// <param name="floor">The Floor (rounded towards negative infinity)</param>

-    /// <param name="ceiling">Ceiling (rounded towards positive infinity)</param>

-    public void FloorCeiling(out BigNum floor, out BigNum ceiling) {

-      //TODO: fix for fp functionality

-      BigNum n = Significand;

-      BigNum e = Exponent;

-      if (n.IsZero) {

-        floor = ceiling = n;

-      } else if (BigNum.ZERO <= e) {

-        // it's an integer

-        for (; BigNum.ZERO < e; e = e - one)

-        {

-          n = n * two;

-        }

-        floor = ceiling = n;

-      } else {

-        // it's a non-zero integer, so the ceiling is one more than the floor

-        for (; BigNum.ZERO < e && !n.IsZero; e = e + one)

-        {

-          n = n / two;  // Division rounds towards negative infinity

-        }

-

-        if (!IsNegative) {

-          floor = n;

-          ceiling = n + one;

-        } else {

-          ceiling = n;

-          floor = n - one;

-        }

-      }

-      Debug.Assert(floor <= ceiling, "Invariant was not maintained");

-    }

-

-    [Pure]

-    public String ToDecimalString(int maxDigits) {

-      //TODO: fix for fp functionality 

-      {

-        throw new NotImplementedException();

-      }

-    }

-

-    public String ToBVString(){

-      if (this.IsSpecialType) {

-        return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize;

-      }

-      else if (this.Value == "") {

-        return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")";

-      }

-      else {

-        return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")";

-      }

-    }

-

-    [Pure]

-    public string ToDecimalString() {

-      Contract.Ensures(Contract.Result<string>() != null);

-      return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;

-    }

-

-    [Pure]

-    public static string Zeros(int n) {

-      //TODO: fix for fp functionality

-      Contract.Requires(0 <= n);

-      if (n <= 10) {

-        var tenZeros = "0000000000";

-        return tenZeros.Substring(0, n);

-      } else {

-        var d = n / 2;

-        var s = Zeros(d);

-        if (n % 2 == 0) {

-          return s + s;

-        } else {

-          return s + s + "0";

-        }

-      }

-    }

-

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Basic arithmetic operations

-

-    [Pure]

-    public BigFloat Abs {

-      get {

-        return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize);

-      }

-    }

-

-    [Pure]

-    public BigFloat Negate {

-      get {

-        if (value != "")

-          return value[0] == '-' ? new BigFloat(value.Remove(0, 1), ExponentSize, significandSize) : new BigFloat("-" + value, ExponentSize, significandSize);

-        return new BigFloat(!isNeg, Exponent, Significand, ExponentSize, SignificandSize);

-      }

-    }

-

-    [Pure]

-    public static BigFloat operator -(BigFloat x) {

-      return x.Negate;

-    }

-

-    [Pure]

-    public static BigFloat operator +(BigFloat x, BigFloat y) {

-      //TODO: Modify for correct fp functionality

-      Contract.Requires(x.ExponentSize == y.ExponentSize);

-      Contract.Requires(x.significandSize == y.significandSize);

-      BigNum m1 = x.significand;

-      BigNum e1 = x.Exponent;

-      BigNum m2 = y.significand;

-      BigNum e2 = y.Exponent;

-      m1 = m1 + two_n(x.significandSize + 1); //Add implicit bit

-      m2 = m2 + two_n(y.significandSize + 1);

-      if (e2 > e1) {

-        m1 = y.significand;

-        e1 = y.Exponent;

-        m2 = x.significand;

-        e2 = x.Exponent;

-      }

-

-      while (e2 < e1) {

-        m2 = m2 / two;

-        e2 = e2 + one;

-      }

-

-      return new BigFloat(false, e1, m1 + m2, x.significandSize, x.ExponentSize);

-    }

-

-    [Pure]

-    public static BigFloat operator -(BigFloat x, BigFloat y) {

-      return x + y.Negate;

-    }

-

-    [Pure]

-    public static BigFloat operator *(BigFloat x, BigFloat y) {

-      Contract.Requires(x.ExponentSize == y.ExponentSize);

-      Contract.Requires(x.significandSize == y.significandSize);

-      return new BigFloat(x.isNeg ^ y.isNeg, x.Exponent + y.Exponent, x.significand * y.significand, x.significandSize, x.ExponentSize);

-    }

-

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Some basic comparison operations

-

-    public bool IsSpecialType {

-      get {

-        if (value == "")

-          return false;

-        return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("zero") || value.Equals("-zero"));

-      }

-    }

-

-    public bool IsPositive {

-      get {

-        return !IsNegative;

-      }

-    }

-

-    public bool IsZero {

-      get {

-        return significand.Equals(BigNum.ZERO) && Exponent == BigNum.ZERO;

-      }

-    }

-

-    [Pure]

-    public int CompareTo(BigFloat that) {

-      if (this.exponent > that.exponent)

-        return 1;

-      if (this.exponent < that.exponent)

-        return -1;

-      if (this.significand == that.significand)

-        return 0;

-      return this.significand > that.significand ? 1 : -1;

-    }

-

-    [Pure]

-    public static bool operator ==(BigFloat x, BigFloat y) {

-      return x.CompareTo(y) == 0;

-    }

-

-    [Pure]

-    public static bool operator !=(BigFloat x, BigFloat y) {

-      return x.CompareTo(y) != 0;

-    }

-

-    [Pure]

-    public static bool operator <(BigFloat x, BigFloat y) {

-      return x.CompareTo(y) < 0;

-    }

-

-    [Pure]

-    public static bool operator >(BigFloat x, BigFloat y) {

-      return x.CompareTo(y) > 0;

-    }

-

-    [Pure]

-    public static bool operator <=(BigFloat x, BigFloat y) {

-      return x.CompareTo(y) <= 0;

-    }

-

-    [Pure]

-    public static bool operator >=(BigFloat x, BigFloat y) {

-      return x.CompareTo(y) >= 0;

-    }

-  }

-}

+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+namespace Microsoft.Basetypes
+{
+  using BIM = System.Numerics.BigInteger;
+    
+  /// <summary>
+  /// A representation of a 32-bit floating point value
+  /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit significand
+  /// </summary>
+  public struct BigFloat
+  {
+    //Please note that this code outline is copy-pasted from BigDec.cs
+
+    // the internal representation
+    [Rep]
+    internal readonly BIM significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left)
+    [Rep]
+    internal readonly int significandSize;
+    [Rep]
+    internal readonly BIM exponent; //The value of the exponent is always positive as per fp representation requirements
+    [Rep]
+    internal readonly int exponentSize; //The bit size of the exponent
+    [Rep]
+    internal readonly String value; //Only used with second syntax
+    [Rep]
+    internal readonly bool isNeg;
+
+    public BIM Significand {
+      get {
+        return significand;
+      }
+    }
+
+    public BIM Exponent {
+      get {
+        return exponent;
+      }
+    }
+
+    public int SignificandSize {
+      get {
+        return significandSize;
+      }
+    }
+
+    public int ExponentSize {
+      get {
+        return exponentSize;
+      }
+    }
+
+    public bool IsNegative {
+      get {
+        return this.isNeg;
+      }
+    }
+
+    public String Value {
+      get {
+        return value;
+      }
+    }
+
+    public static BigFloat ZERO = new BigFloat(false, BIM.Zero, BIM.Zero, 24, 8); //Does not include negative zero
+
+    private static readonly BIM two = new BIM(2);
+    private static readonly BIM one = new BIM(1);
+    private static BIM two_n(int n) {
+      BIM toReturn = one;
+      for (int i = 0; i < n; i++)
+        toReturn = toReturn * two;
+      return toReturn;
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Constructors
+
+    //Please note that these constructors will be called throughout boogie
+    //For a complete summary of where this class has been added, simply view constructor references
+
+    [Pure]
+    public static BigFloat FromInt(int v) {
+      return new BigFloat(v.ToString(), 24, 8);
+    }
+
+    public static BigFloat FromInt(int v, int significandSize, int exponentSize)
+    {
+      return new BigFloat(v.ToString(), significandSize, exponentSize);
+    }
+
+    public static BigFloat FromBigInt(BIM v) {
+      return new BigFloat(v.ToString(), 24, 8);
+    }
+
+    public static BigFloat FromBigInt(BIM v, int significandSize, int exponentSize)
+    {
+      return new BigFloat(v.ToString(), significandSize, exponentSize);
+    }
+
+    public static BigFloat FromBigDec(BigDec v)
+    {
+      return new BigFloat(v.ToDecimalString(), 24, 8);
+    }
+
+    public static BigFloat FromBigDec(BigDec v, int significandSize, int exponentSize)
+    {
+      return new BigFloat(v.ToDecimalString(), significandSize, exponentSize);
+    }
+
+    [Pure]
+    public static BigFloat FromString(String s) {
+      /*
+       * String must be either of the format *e*f*e*
+       * or of the special value formats: 0NaN*e* 0nan*e* 0+oo*e* 0-oo*e*
+       * Where * indicates an integer value (digit)
+       */
+      BIM sig, exp;
+      int sigSize, expSize;
+      bool isNeg;
+
+      if (s.IndexOf('f') == -1) {
+        String val = s;
+        sigSize = int.Parse(s.Substring(4, s.IndexOf('e')-4));
+        expSize = int.Parse(s.Substring(s.IndexOf('e') + 1));
+        if (sigSize <= 0 || expSize <= 0)
+          throw new FormatException("Significand and Exponent sizes must be greater than 0");
+        return new BigFloat(val, sigSize, expSize);
+      }
+
+      sig = BIM.Parse(s.Substring(0, s.IndexOf('e')));
+      exp = BIM.Parse(s.Substring(s.IndexOf('e') + 1, s.IndexOf('f') - s.IndexOf('e') - 1));
+      sigSize = int.Parse(s.Substring(s.IndexOf('f') + 1, s.IndexOf('e', s.IndexOf('e') + 1) - s.IndexOf('f') - 1));
+      expSize = int.Parse(s.Substring(s.IndexOf('e', s.IndexOf('e') + 1) + 1));
+      
+      if (sigSize <= 0 || expSize <= 0)
+        throw new FormatException("Significand and Exponent sizes must be greater than 0");
+
+      sigSize = sigSize - 1; //Get rid of sign bit
+      isNeg = sig < 0;
+      sig = BIM.Abs(sig);
+      exp = exp + BIM.Pow(new BIM(2), expSize-1) - BIM.One;
+
+      if (exp < 0 || exp >= BIM.Pow(new BIM(2), expSize))
+        throw new FormatException("The given exponent " + exp + " cannot fit in the bit size " + expSize);
+
+      if (sig >= BIM.Pow(new BIM(2), sigSize))
+        throw new FormatException("The given significand " + sig + " cannot fit in the bit size " + (sigSize+1));
+
+      return new BigFloat(isNeg, sig, exp, sigSize, expSize);
+    }
+
+    public BigFloat(bool isNeg, BIM significand, BIM exponent, int significandSize, int exponentSize) {
+      this.exponentSize = exponentSize;
+      this.exponent = exponent;
+      this.significand = significand;
+      this.significandSize = significandSize+1;
+      this.isNeg = isNeg;
+      this.value = "";
+    }
+
+    public BigFloat(String value, int significandSize, int exponentSize) {
+      this.exponentSize = exponentSize;
+      this.significandSize = significandSize;
+      this.exponent = BIM.Zero;
+      this.significand = BIM.Zero;
+      this.value = value;
+      if (value.Equals("nan"))
+        this.value = "NaN";
+      this.isNeg = value[0] == '-';
+    }
+
+    private BIM maxsignificand()
+    {
+      BIM result = one;
+      for (int i = 0; i < significandSize; i++)
+        result = result * two;
+      return result - one;
+    }
+    private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; }
+
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Basic object operations
+
+    [Pure]
+    [Reads(ReadsAttribute.Reads.Nothing)]
+    public override bool Equals(object obj) {
+      if (obj == null)
+        return false;
+      if (!(obj is BigFloat))
+        return false;
+
+      return (this == (BigFloat)obj);
+    }
+
+    [Pure]
+    public override int GetHashCode() {
+      return significand.GetHashCode() * 13 + Exponent.GetHashCode();
+    }
+
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Conversion operations
+
+    /// <summary>
+    /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!
+    /// Converts the given decimal value (provided as a string) to the nearest floating point approximation
+    /// the returned fp assumes the given significand and exponent size
+    /// </summary>
+    /// <param name="value"></param>
+    /// <param name="significandSize"></param>
+    /// <param name="exponentSize"></param>
+    /// <returns></returns>
+    public static BigFloat Round(String value, int exponentSize, int significandSize)
+    {
+      int i = value.IndexOf('.');
+      if (i == -1)
+        return Round(BIM.Parse(value), BIM.Zero, exponentSize, significandSize);
+      return Round(i == 0 ? BIM.Zero : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), exponentSize, significandSize);
+    }
+
+    /// <summary>
+    /// NOTE:  THIS METHOD MAY NOT WORK AS EXPECTED!!!!
+    /// Converts value.dec_value to a the closest float approximation with the given significandSize, exponentSize
+    /// Returns the result of this calculation
+    /// </summary>
+    /// <param name="value"></param>
+    /// <param name="power"></param>
+    /// <param name="significandSize"></param>
+    /// <param name="exponentSize"></param>
+    /// <returns></returns>
+    public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int significandSize)
+    {
+      int exp = 0;
+      BIM one = new BIM(1);
+      BIM ten = new BIM(10);
+      BIM dec_max = new BIM(0); //represents the order of magnitude of dec_value for carrying during calculations
+
+      //First, determine the exponent
+      while (value > one) { //Divide by two, increment exponent by 1
+        if (!(value % two).IsZero) { //Add "1.0" to the decimal
+          dec_max = new BIM(10);
+          while (dec_max < dec_value)
+            dec_max = dec_max * ten;
+          dec_value = dec_value + dec_max;
+        }
+        value = value / two;
+        if (!(dec_value % ten).IsZero)
+          dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division
+        dec_value = dec_value / two;
+        exp++;
+      }
+      if (value.IsZero && !dec_value.IsZero) {
+        dec_max = new BIM(10);
+        while (dec_max < dec_value)
+          dec_max = dec_max * ten;
+        while (value.IsZero) {//Multiply by two, decrement exponent by 1
+          dec_value = dec_value * two;
+          if (dec_value >= dec_max) {
+            dec_value = dec_value - dec_max;
+            value = value + one;
+          }
+          exp--;
+        }
+      }
+
+      //Second, calculate the significand
+      value = new BIM(0); //remove implicit bit
+      dec_max = new BIM(10);
+      while (dec_max < dec_value)
+        dec_max = dec_max * ten;
+      for (int i = significandSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the significand is fully calculated
+        dec_value = dec_value * two;
+        if (dec_value >= dec_max) {
+          dec_value = dec_value - dec_max;
+          value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation
+        }
+      }
+
+      return new BigFloat(false, BIM.Zero, BIM.Parse(value.ToString()), exponentSize, significandSize); //Sign not actually checked...
+    }
+
+    // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
+    /// <summary>
+    /// NOTE:  This may give wrong results, it hasn't been tested extensively
+    /// If you're getting weird bugs, you may want to check this function out...
+    /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative
+    /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.
+    /// </summary>
+    /// <param name="floor">The Floor (rounded towards negative infinity)</param>
+    /// <param name="ceiling">Ceiling (rounded towards positive infinity)</param>
+    public void FloorCeiling(out BIM floor, out BIM ceiling)
+    {
+      BIM two = new BIM(2);
+
+      BIM sig = Significand + BIM.Pow(two, SignificandSize); //Add hidden bit
+      BIM exp = Exponent - BIM.Pow(two, ExponentSize);
+      sig = sig >> ExponentSize;
+
+      while (exp > BIM.Zero) {
+        exp--;
+        sig = sig >> 1;
+      }
+
+      if (isNeg) {
+        ceiling = -sig + 1;
+        floor = -sig;
+      }
+      else {
+        ceiling = sig + 1;
+        floor = sig;
+      }
+    }
+
+    [Pure]
+    public String ToDecimalString(int maxDigits) {
+      //TODO: fix for fp functionality 
+      {
+        throw new NotImplementedException();
+      }
+    }
+
+    public String ToBVString(){
+      if (this.IsSpecialType) {
+        return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize;
+      }
+      else if (this.Value == "") {
+        return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")";
+      }
+      else {
+        return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")";
+      }
+    }
+
+    [Pure]
+    public string ToDecimalString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
+    }
+
+    [Pure]
+    public static string Zeros(int n) {
+      //TODO: fix for fp functionality
+      Contract.Requires(0 <= n);
+      if (n <= 10) {
+        var tenZeros = "0000000000";
+        return tenZeros.Substring(0, n);
+      } else {
+        var d = n / 2;
+        var s = Zeros(d);
+        if (n % 2 == 0) {
+          return s + s;
+        } else {
+          return s + s + "0";
+        }
+      }
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Basic arithmetic operations
+
+    [Pure]
+    public BigFloat Abs {
+      get {
+        return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize);
+      }
+    }
+
+    [Pure]
+    public BigFloat Negate {
+      get {
+        if (value != "")
+          return value[0] == '-' ? new BigFloat(value.Remove(0, 1), ExponentSize, significandSize) : new BigFloat("-" + value, ExponentSize, significandSize);
+        return new BigFloat(!isNeg, Exponent, Significand, ExponentSize, SignificandSize);
+      }
+    }
+
+    [Pure]
+    public static BigFloat operator -(BigFloat x) {
+      return x.Negate;
+    }
+
+    [Pure]
+    public static BigFloat operator +(BigFloat x, BigFloat y) {
+      //TODO: Modify for correct fp functionality
+      Contract.Requires(x.ExponentSize == y.ExponentSize);
+      Contract.Requires(x.significandSize == y.significandSize);
+      BIM m1 = x.significand;
+      BIM e1 = x.Exponent;
+      BIM m2 = y.significand;
+      BIM e2 = y.Exponent;
+      m1 = m1 + two_n(x.significandSize + 1); //Add implicit bit
+      m2 = m2 + two_n(y.significandSize + 1);
+      if (e2 > e1) {
+        m1 = y.significand;
+        e1 = y.Exponent;
+        m2 = x.significand;
+        e2 = x.Exponent;
+      }
+
+      while (e2 < e1) {
+        m2 = m2 / two;
+        e2 = e2 + one;
+      }
+
+      return new BigFloat(false, e1, m1 + m2, x.significandSize, x.ExponentSize);
+    }
+
+    [Pure]
+    public static BigFloat operator -(BigFloat x, BigFloat y) {
+      return x + y.Negate;
+    }
+
+    [Pure]
+    public static BigFloat operator *(BigFloat x, BigFloat y) {
+      Contract.Requires(x.ExponentSize == y.ExponentSize);
+      Contract.Requires(x.significandSize == y.significandSize);
+      return new BigFloat(x.isNeg ^ y.isNeg, x.Exponent + y.Exponent, x.significand * y.significand, x.significandSize, x.ExponentSize);
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Some basic comparison operations
+
+    public bool IsSpecialType {
+      get {
+        if (value == "")
+          return false;
+        return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("zero") || value.Equals("-zero"));
+      }
+    }
+
+    public bool IsPositive {
+      get {
+        return !IsNegative;
+      }
+    }
+
+    public bool IsZero {
+      get {
+        return significand.Equals(BigNum.ZERO) && Exponent == BIM.Zero;
+      }
+    }
+
+    [Pure]
+    public int CompareTo(BigFloat that) {
+      if (this.exponent > that.exponent)
+        return 1;
+      if (this.exponent < that.exponent)
+        return -1;
+      if (this.significand == that.significand)
+        return 0;
+      return this.significand > that.significand ? 1 : -1;
+    }
+
+    [Pure]
+    public static bool operator ==(BigFloat x, BigFloat y) {
+      return x.CompareTo(y) == 0;
+    }
+
+    [Pure]
+    public static bool operator !=(BigFloat x, BigFloat y) {
+      return x.CompareTo(y) != 0;
+    }
+
+    [Pure]
+    public static bool operator <(BigFloat x, BigFloat y) {
+      return x.CompareTo(y) < 0;
+    }
+
+    [Pure]
+    public static bool operator >(BigFloat x, BigFloat y) {
+      return x.CompareTo(y) > 0;
+    }
+
+    [Pure]
+    public static bool operator <=(BigFloat x, BigFloat y) {
+      return x.CompareTo(y) <= 0;
+    }
+
+    [Pure]
+    public static bool operator >=(BigFloat x, BigFloat y) {
+      return x.CompareTo(y) >= 0;
+    }
+  }
+}
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index bc2b4391..409254d0 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -584,7 +584,7 @@ namespace Microsoft.Boogie {
     {
       Contract.Requires(tok != null);
       Val = v;
-      Type = Type.GetFloatType(v.ExponentSize, v.SignificandSize);
+      Type = Type.GetFloatType(v.SignificandSize, v.ExponentSize);
       if (immutable)
         CachedHashCode = ComputeHashCode();
     }
@@ -662,7 +662,7 @@ namespace Microsoft.Boogie {
           return Type.Real;
         } else if (Val is BigFloat) {
           BigFloat temp = (BigFloat)Val;
-          return Type.GetFloatType(temp.ExponentSize, temp.SignificandSize);
+          return Type.GetFloatType(temp.SignificandSize, temp.ExponentSize);
         } else if (Val is BvConst) {
           return Type.GetBvType(((BvConst)Val).Bits);
         } else {
@@ -1724,10 +1724,10 @@ namespace Microsoft.Boogie {
             return Type.Real;
           }
           if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
-            return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatSignificand);
+            return Type.GetFloatType(arg0.Type.FloatSignificand, arg0.Type.FloatExponent);
           }
           if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
-            return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatSignificand);
+            return Type.GetFloatType(arg1.Type.FloatSignificand, arg1.Type.FloatExponent);
           }
           goto BAD_TYPE;
         case Opcode.Div:
@@ -1742,10 +1742,10 @@ namespace Microsoft.Boogie {
             return Type.Real;
           }
           if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
-            return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatSignificand);
+            return Type.GetFloatType(arg0.Type.FloatSignificand, arg0.Type.FloatExponent);
           }
           if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
-            return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatSignificand);
+            return Type.GetFloatType(arg1.Type.FloatSignificand, arg1.Type.FloatExponent);
           }
           goto BAD_TYPE;
         case Opcode.Pow:
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 08cf37cc..ab6ef5e9 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -386,12 +386,12 @@ namespace Microsoft.Boogie {
       }
     }
 
-    static public FloatType GetFloatType(int exp, int man) {
+    static public FloatType GetFloatType(int sig, int exp) {
       Contract.Requires(0 <= exp);
-      Contract.Requires(0 <= man);
+      Contract.Requires(0 <= sig);
       Contract.Ensures(Contract.Result<FloatType>() != null);
 
-      return new FloatType(exp, man);
+      return new FloatType(sig, exp);
     }
 
     //------------ Match formal argument types on actual argument types
@@ -1094,7 +1094,7 @@ namespace Microsoft.Boogie {
     public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
-      return "float (" + Exponent + " " + Significand + ")";
+      return "float" + Significand + "e" + Exponent;
     }
 
     //-----------  Equality  ----------------------------------
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 091ceeb0..31823110 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -144,7 +144,8 @@ TOKENS
   string = quote { regularStringChar | "\\\"" } quote.
 
   decimal = digit {digit} 'e' [ '-' ] digit {digit} .
-  float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] .
+  dec_float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] .
+		float = digit {digit} 'e' digit {digit} 'f' digit {digit} 'e' digit {digit} .
 
 COMMENTS FROM "/*" TO "*/" NESTED
 COMMENTS FROM "//" TO lf
@@ -330,7 +331,7 @@ TypeAtom<out Bpl.Type/*!*/ ty>
   ( "int"              (. ty = new BasicType(t, SimpleType.Int); .)
   | "real"             (. ty = new BasicType(t, SimpleType.Real); .)
   | "bool"             (. ty = new BasicType(t, SimpleType.Bool); .)
-  /* note: bitvectors are handled in UnresolvedTypeIdentifier */
+  /* note: bitvectors and floats are handled in UnresolvedTypeIdentifier */
   |
   "("
   Type<out ty>
@@ -1252,7 +1253,7 @@ ArrayExpression<out Expr/*!*/ e>
 
 /*------------------------------------------------------------------------*/
 AtomExpression<out Expr/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat bf;
      List<Expr>/*!*/ es;  List<Variable>/*!*/ ds;  Trigger trig;
      List<TypeVariable>/*!*/ typeParams;
      IdentifierExpr/*!*/ id;
@@ -1265,6 +1266,7 @@ AtomExpression<out Expr/*!*/ e>
   | "true"            (. e = new LiteralExpr(t, true); .)
   | Nat<out bn>            (. e = new LiteralExpr(t, bn); .)
   | Dec<out bd>            (. e = new LiteralExpr(t, bd); .)
+		| Float<out bf>            (. e = new LiteralExpr(t, bf); .)
   | BvLit<out bn, out n> (. e = new LiteralExpr(t, bn, n); .)
 
   | Ident<out x>            (. id = new IdentifierExpr(x, x.val);  e = id; .)
@@ -1479,7 +1481,7 @@ Dec<out BigDec n>
   (
     decimal   (. s = t.val; .)
   |
-    float     (. s = t.val; .)
+    dec_float     (. s = t.val; .)
   )
   (. try {
        n = BigDec.FromString(s);
@@ -1508,4 +1510,19 @@ BvLit<out BigNum n, out int m>
      }
   .)
   .
+
+Float<out BigFloat n>
+= (. string s = ""; .)
+  (
+    float   (. s = t.val; .)
+  )
+  (. try {
+       n = BigFloat.FromString(s);
+     } catch (FormatException) {
+       this.SemErr("incorrectly formatted number");
+       n = BigFloat.ZERO;
+     }
+  .)
+  .
+
 END BoogiePL.
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 78823b61..a5e2921e 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -23,8 +23,9 @@ public class Parser {
 	public const int _digits = 3;
 	public const int _string = 4;
 	public const int _decimal = 5;
-	public const int _float = 6;
-	public const int maxT = 96;
+	public const int _dec_float = 6;
+	public const int _float = 7;
+	public const int maxT = 97;
 
 	const bool T = true;
 	const bool x = false;
@@ -117,7 +118,7 @@ private class BvBounds : Expr {
   public BigNum Lower;
   public BigNum Upper;
   public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper)
-    : base(tok, /*immutable*/ false) {
+    : base(tok, /*immutable=*/ false) {
     Contract.Requires(tok != null);
     this.Lower = lower;
     this.Upper = upper;
@@ -132,8 +133,7 @@ private class BvBounds : Expr {
     Contract.Assert(false);throw new cce.UnreachableException();
   }
   public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); }
-  public override int ComputeHashCode()
-  {
+  public override int ComputeHashCode() {
     return base.GetHashCode();
   }
 }
@@ -220,7 +220,7 @@ private class BvBounds : Expr {
 		
 		while (StartOf(1)) {
 			switch (la.kind) {
-			case 21: {
+			case 22: {
 				Consts(out vs);
 				foreach(Bpl.Variable/*!*/ v in vs){
 				 Contract.Assert(v != null);
@@ -229,7 +229,7 @@ private class BvBounds : Expr {
 				
 				break;
 			}
-			case 25: {
+			case 26: {
 				Function(out ds);
 				foreach(Bpl.Declaration/*!*/ d in ds){
 				 Contract.Assert(d != null);
@@ -238,12 +238,12 @@ private class BvBounds : Expr {
 				
 				break;
 			}
-			case 29: {
+			case 30: {
 				Axiom(out ax);
 				Pgm.AddTopLevelDeclaration(ax); 
 				break;
 			}
-			case 30: {
+			case 31: {
 				UserDefinedTypes(out ts);
 				foreach(Declaration/*!*/ td in ts){
 				 Contract.Assert(td != null);
@@ -252,7 +252,7 @@ private class BvBounds : Expr {
 				
 				break;
 			}
-			case 7: {
+			case 8: {
 				GlobalVars(out vs);
 				foreach(Bpl.Variable/*!*/ v in vs){
 				 Contract.Assert(v != null);
@@ -261,7 +261,7 @@ private class BvBounds : Expr {
 				
 				break;
 			}
-			case 32: {
+			case 33: {
 				Procedure(out pr, out im);
 				Pgm.AddTopLevelDeclaration(pr);
 				if (im != null) {
@@ -270,7 +270,7 @@ private class BvBounds : Expr {
 				
 				break;
 			}
-			case 33: {
+			case 34: {
 				Implementation(out nnim);
 				Pgm.AddTopLevelDeclaration(nnim); 
 				break;
@@ -286,17 +286,17 @@ private class BvBounds : Expr {
 		bool u = false; QKeyValue kv = null;
 		bool ChildrenComplete = false;
 		List<ConstantParent/*!*/> Parents = null; 
-		Expect(21);
+		Expect(22);
 		y = t; 
-		while (la.kind == 27) {
+		while (la.kind == 28) {
 			Attribute(ref kv);
 		}
-		if (la.kind == 22) {
+		if (la.kind == 23) {
 			Get();
 			u = true;  
 		}
 		IdsType(out xs);
-		if (la.kind == 23) {
+		if (la.kind == 24) {
 			OrderSpec(out ChildrenComplete, out Parents);
 		}
 		bool makeClone = false;
@@ -320,7 +320,7 @@ private class BvBounds : Expr {
 		 ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));
 		}
 		
-		Expect(8);
+		Expect(9);
 	}
 
 	void Function(out List<Declaration>/*!*/ ds) {
@@ -337,44 +337,44 @@ private class BvBounds : Expr {
 		Expr definition = null;
 		Expr/*!*/ tmp;
 		
-		Expect(25);
-		while (la.kind == 27) {
+		Expect(26);
+		while (la.kind == 28) {
 			Attribute(ref kv);
 		}
 		Ident(out z);
-		if (la.kind == 19) {
+		if (la.kind == 20) {
 			TypeParams(out typeParamTok, out typeParams);
 		}
-		Expect(9);
+		Expect(10);
 		if (StartOf(2)) {
 			VarOrType(out tyd, out argKv);
 			arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); 
-			while (la.kind == 12) {
+			while (la.kind == 13) {
 				Get();
 				VarOrType(out tyd, out argKv);
 				arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); 
 			}
 		}
-		Expect(10);
+		Expect(11);
 		argKv = null; 
-		if (la.kind == 26) {
+		if (la.kind == 27) {
 			Get();
-			Expect(9);
-			VarOrType(out retTyd, out argKv);
 			Expect(10);
-		} else if (la.kind == 11) {
+			VarOrType(out retTyd, out argKv);
+			Expect(11);
+		} else if (la.kind == 12) {
 			Get();
 			Type(out retTy);
 			retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); 
-		} else SynErr(97);
-		if (la.kind == 27) {
+		} else SynErr(98);
+		if (la.kind == 28) {
 			Get();
 			Expression(out tmp);
 			definition = tmp; 
-			Expect(28);
-		} else if (la.kind == 8) {
+			Expect(29);
+		} else if (la.kind == 9) {
 			Get();
-		} else SynErr(98);
+		} else SynErr(99);
 		if (retTyd == null) {
 		 // construct a dummy type for the case of syntax error
 		 retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
@@ -429,30 +429,30 @@ private class BvBounds : Expr {
 
 	void Axiom(out Axiom/*!*/ m) {
 		Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; 
-		Expect(29);
-		while (la.kind == 27) {
+		Expect(30);
+		while (la.kind == 28) {
 			Attribute(ref kv);
 		}
 		IToken/*!*/ x = t; 
 		Proposition(out e);
-		Expect(8);
+		Expect(9);
 		m = new Axiom(x,e, null, kv); 
 	}
 
 	void UserDefinedTypes(out List<Declaration/*!*/>/*!*/ ts) {
 		Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> (); 
-		Expect(30);
-		while (la.kind == 27) {
+		Expect(31);
+		while (la.kind == 28) {
 			Attribute(ref kv);
 		}
 		UserDefinedType(out decl, kv);
 		ts.Add(decl);  
-		while (la.kind == 12) {
+		while (la.kind == 13) {
 			Get();
 			UserDefinedType(out decl, kv);
 			ts.Add(decl);  
 		}
-		Expect(8);
+		Expect(9);
 	}
 
 	void GlobalVars(out List<Variable>/*!*/ ds) {
@@ -461,12 +461,12 @@ private class BvBounds : Expr {
 		ds = new List<Variable>();
 		var dsx = ds;
 		
-		Expect(7);
-		while (la.kind == 27) {
+		Expect(8);
+		while (la.kind == 28) {
 			Attribute(ref kv);
 		}
 		IdsTypeWheres(true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } );
-		Expect(8);
+		Expect(9);
 	}
 
 	void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) {
@@ -482,9 +482,9 @@ private class BvBounds : Expr {
 		QKeyValue kv = null;
 		impl = null;
 		
-		Expect(32);
+		Expect(33);
 		ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);
-		if (la.kind == 8) {
+		if (la.kind == 9) {
 			Get();
 			while (StartOf(3)) {
 				Spec(pre, mods, post);
@@ -497,7 +497,7 @@ private class BvBounds : Expr {
 			impl = new Implementation(x, x.val, typeParams,
 			                         Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
 			
-		} else SynErr(99);
+		} else SynErr(100);
 		proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); 
 	}
 
@@ -509,7 +509,7 @@ private class BvBounds : Expr {
 		StmtList/*!*/ stmtList;
 		QKeyValue kv;
 		
-		Expect(33);
+		Expect(34);
 		ProcSignature(false, out x, out typeParams, out ins, out outs, out kv);
 		ImplBody(out locals, out stmtList);
 		impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); 
@@ -523,7 +523,7 @@ private class BvBounds : Expr {
 
 	void IdsTypeWheres(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) {
 		IdsTypeWhere(allowWhereClauses, context, action);
-		while (la.kind == 12) {
+		while (la.kind == 13) {
 			Get();
 			IdsTypeWhere(allowWhereClauses, context, action);
 		}
@@ -533,12 +533,12 @@ private class BvBounds : Expr {
 		Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
 		QKeyValue kv = null;
 		
-		Expect(7);
-		while (la.kind == 27) {
+		Expect(8);
+		while (la.kind == 28) {
 			Attribute(ref kv);
 		}
 		IdsTypeWheres(true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } );
-		Expect(8);
+		Expect(9);
 	}
 
 	void ProcFormals(bool incoming, bool allowWhereClauses, out List<Variable>/*!*/ ds) {
@@ -547,16 +547,16 @@ private class BvBounds : Expr {
 		var dsx = ds;
 		var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals";
 		
-		Expect(9);
-		if (la.kind == 1 || la.kind == 27) {
+		Expect(10);
+		if (la.kind == 1 || la.kind == 28) {
 			AttrsIdsTypeWheres(allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); });
 		}
-		Expect(10);
+		Expect(11);
 	}
 
 	void AttrsIdsTypeWheres(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
 		AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action);
-		while (la.kind == 12) {
+		while (la.kind == 13) {
 			Get();
 			AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action);
 		}
@@ -575,7 +575,7 @@ private class BvBounds : Expr {
 	void IdsType(out List<TypedIdent>/*!*/ tyds) {
 		Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List<IToken>/*!*/ ids;  Bpl.Type/*!*/ ty; 
 		Idents(out ids);
-		Expect(11);
+		Expect(12);
 		Type(out ty);
 		tyds = new List<TypedIdent>();
 		foreach(Token/*!*/ id in ids){
@@ -589,7 +589,7 @@ private class BvBounds : Expr {
 		Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); 
 		Ident(out id);
 		xs.Add(id); 
-		while (la.kind == 12) {
+		while (la.kind == 13) {
 			Get();
 			Ident(out id);
 			xs.Add(id); 
@@ -607,14 +607,14 @@ private class BvBounds : Expr {
 				TypeArgs(args);
 			}
 			ty = new UnresolvedTypeIdentifier (tok, tok.val, args); 
-		} else if (la.kind == 17 || la.kind == 19) {
+		} else if (la.kind == 18 || la.kind == 20) {
 			MapType(out ty);
-		} else SynErr(100);
+		} else SynErr(101);
 	}
 
 	void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
 		QKeyValue kv = null; 
-		while (la.kind == 27) {
+		while (la.kind == 28) {
 			Attribute(ref kv);
 			if (!allowAttributes) {
 			 kv = null;
@@ -628,9 +628,9 @@ private class BvBounds : Expr {
 	void IdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) {
 		List<IToken>/*!*/ ids;  Bpl.Type/*!*/ ty;  Expr wh = null;  Expr/*!*/ nne; 
 		Idents(out ids);
-		Expect(11);
+		Expect(12);
 		Type(out ty);
-		if (la.kind == 13) {
+		if (la.kind == 14) {
 			Get();
 			Expression(out nne);
 			if (!allowWhereClauses) {
@@ -650,7 +650,7 @@ private class BvBounds : Expr {
 	void Expression(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		ImpliesExpression(false, out e0);
-		while (la.kind == 55 || la.kind == 56) {
+		while (la.kind == 56 || la.kind == 57) {
 			EquivOp();
 			x = t; 
 			ImpliesExpression(false, out e1);
@@ -660,20 +660,20 @@ private class BvBounds : Expr {
 
 	void TypeAtom(out Bpl.Type/*!*/ ty) {
 		Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType; 
-		if (la.kind == 14) {
+		if (la.kind == 15) {
 			Get();
 			ty = new BasicType(t, SimpleType.Int); 
-		} else if (la.kind == 15) {
+		} else if (la.kind == 16) {
 			Get();
 			ty = new BasicType(t, SimpleType.Real); 
-		} else if (la.kind == 16) {
+		} else if (la.kind == 17) {
 			Get();
 			ty = new BasicType(t, SimpleType.Bool); 
-		} else if (la.kind == 9) {
+		} else if (la.kind == 10) {
 			Get();
 			Type(out ty);
-			Expect(10);
-		} else SynErr(101);
+			Expect(11);
+		} else SynErr(102);
 	}
 
 	void Ident(out IToken/*!*/ x) {
@@ -700,10 +700,10 @@ private class BvBounds : Expr {
 			if (StartOf(6)) {
 				TypeArgs(ts);
 			}
-		} else if (la.kind == 17 || la.kind == 19) {
+		} else if (la.kind == 18 || la.kind == 20) {
 			MapType(out ty);
 			ts.Add(ty); 
-		} else SynErr(102);
+		} else SynErr(103);
 	}
 
 	void MapType(out Bpl.Type/*!*/ ty) {
@@ -713,16 +713,16 @@ private class BvBounds : Expr {
 		Bpl.Type/*!*/ result;
 		List<TypeVariable>/*!*/ typeParameters = new List<TypeVariable>();
 		
-		if (la.kind == 19) {
+		if (la.kind == 20) {
 			TypeParams(out nnTok, out typeParameters);
 			tok = nnTok; 
 		}
-		Expect(17);
+		Expect(18);
 		if (tok == null) tok = t;  
 		if (StartOf(6)) {
 			Types(arguments);
 		}
-		Expect(18);
+		Expect(19);
 		Type(out result);
 		ty = new MapType(tok, typeParameters, arguments, result);
 		
@@ -730,10 +730,10 @@ private class BvBounds : Expr {
 
 	void TypeParams(out IToken/*!*/ tok, out List<TypeVariable>/*!*/ typeParams) {
 		Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List<IToken>/*!*/ typeParamToks; 
-		Expect(19);
+		Expect(20);
 		tok = t;  
 		Idents(out typeParamToks);
-		Expect(20);
+		Expect(21);
 		typeParams = new List<TypeVariable> ();
 		foreach(Token/*!*/ id in typeParamToks){
 		 Contract.Assert(id != null);
@@ -745,7 +745,7 @@ private class BvBounds : Expr {
 		Contract.Requires(ts != null); Bpl.Type/*!*/ ty; 
 		Type(out ty);
 		ts.Add(ty); 
-		while (la.kind == 12) {
+		while (la.kind == 13) {
 			Get();
 			Type(out ty);
 			ts.Add(ty); 
@@ -757,21 +757,21 @@ private class BvBounds : Expr {
 		Parents = null;
 		bool u;
 		IToken/*!*/ parent; 
-		Expect(23);
+		Expect(24);
 		Parents = new List<ConstantParent/*!*/> ();
 		u = false; 
-		if (la.kind == 1 || la.kind == 22) {
-			if (la.kind == 22) {
+		if (la.kind == 1 || la.kind == 23) {
+			if (la.kind == 23) {
 				Get();
 				u = true; 
 			}
 			Ident(out parent);
 			Parents.Add(new ConstantParent (
 			           new IdentifierExpr(parent, parent.val), u)); 
-			while (la.kind == 12) {
+			while (la.kind == 13) {
 				Get();
 				u = false; 
-				if (la.kind == 22) {
+				if (la.kind == 23) {
 					Get();
 					u = true; 
 				}
@@ -780,7 +780,7 @@ private class BvBounds : Expr {
 				           new IdentifierExpr(parent, parent.val), u)); 
 			}
 		}
-		if (la.kind == 24) {
+		if (la.kind == 25) {
 			Get();
 			ChildrenComplete = true; 
 		}
@@ -793,12 +793,12 @@ private class BvBounds : Expr {
 		IToken/*!*/ tok;
 		kv = null;
 		
-		while (la.kind == 27) {
+		while (la.kind == 28) {
 			Attribute(ref kv);
 		}
 		Type(out ty);
 		tok = ty.tok; 
-		if (la.kind == 11) {
+		if (la.kind == 12) {
 			Get();
 			var uti = ty as UnresolvedTypeIdentifier;
 			if (uti != null && uti.Arguments.Count == 0) {
@@ -824,7 +824,7 @@ private class BvBounds : Expr {
 		if (la.kind == 1) {
 			WhiteSpaceIdents(out paramTokens);
 		}
-		if (la.kind == 31) {
+		if (la.kind == 32) {
 			Get();
 			Type(out body);
 			synonym = true; 
@@ -856,15 +856,15 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		Contract.Ensures(Contract.ValueAtReturn(out name) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ins) != null); Contract.Ensures(Contract.ValueAtReturn(out outs) != null);
 		IToken/*!*/ typeParamTok; typeParams = new List<TypeVariable>();
 		outs = new List<Variable>(); kv = null; 
-		while (la.kind == 27) {
+		while (la.kind == 28) {
 			Attribute(ref kv);
 		}
 		Ident(out name);
-		if (la.kind == 19) {
+		if (la.kind == 20) {
 			TypeParams(out typeParamTok, out typeParams);
 		}
 		ProcFormals(true, allowWhereClausesOnFormals, out ins);
-		if (la.kind == 26) {
+		if (la.kind == 27) {
 			Get();
 			ProcFormals(false, allowWhereClausesOnFormals, out outs);
 		}
@@ -872,7 +872,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 
 	void Spec(List<Requires>/*!*/ pre, List<IdentifierExpr>/*!*/ mods, List<Ensures>/*!*/ post) {
 		Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List<IToken>/*!*/ ms; 
-		if (la.kind == 34) {
+		if (la.kind == 35) {
 			Get();
 			if (la.kind == 1) {
 				Idents(out ms);
@@ -882,19 +882,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 				}
 				
 			}
-			Expect(8);
-		} else if (la.kind == 35) {
+			Expect(9);
+		} else if (la.kind == 36) {
 			Get();
 			SpecPrePost(true, pre, post);
-		} else if (la.kind == 36 || la.kind == 37) {
+		} else if (la.kind == 37 || la.kind == 38) {
 			SpecPrePost(false, pre, post);
-		} else SynErr(103);
+		} else SynErr(104);
 	}
 
 	void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {
 		Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List<Variable>(); 
-		Expect(27);
-		while (la.kind == 7) {
+		Expect(28);
+		while (la.kind == 8) {
 			LocalVars(locals);
 		}
 		StmtList(out stmtList);
@@ -902,25 +902,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 
 	void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
 		Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; 
-		if (la.kind == 36) {
+		if (la.kind == 37) {
 			Get();
 			tok = t; 
-			while (la.kind == 27) {
+			while (la.kind == 28) {
 				Attribute(ref kv);
 			}
 			Proposition(out e);
-			Expect(8);
+			Expect(9);
 			pre.Add(new Requires(tok, free, e, null, kv)); 
-		} else if (la.kind == 37) {
+		} else if (la.kind == 38) {
 			Get();
 			tok = t; 
-			while (la.kind == 27) {
+			while (la.kind == 28) {
 				Attribute(ref kv);
 			}
 			Proposition(out e);
-			Expect(8);
+			Expect(9);
 			post.Add(new Ensures(tok, free, e, null, kv)); 
-		} else SynErr(104);
+		} else SynErr(105);
 	}
 
 	void StmtList(out StmtList/*!*/ stmtList) {
@@ -957,7 +957,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 				 cs = new List<Cmd>();
 				}
 				
-			} else if (la.kind == 40 || la.kind == 42 || la.kind == 45) {
+			} else if (la.kind == 41 || la.kind == 43 || la.kind == 46) {
 				StructuredCmd(out ecn);
 				ec = ecn;
 				if (startToken == null) { startToken = ec.tok;  cs = new List<Cmd>(); }
@@ -977,7 +977,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 				
 			}
 		}
-		Expect(28);
+		Expect(29);
 		IToken/*!*/ endCurly = t;
 		if (startToken == null && bigblocks.Count == 0) {
 		 startToken = t;  cs = new List<Cmd>();
@@ -1005,33 +1005,33 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 			LabelOrAssign(out c, out label);
 			break;
 		}
-		case 46: {
+		case 47: {
 			Get();
 			x = t; 
-			while (la.kind == 27) {
+			while (la.kind == 28) {
 				Attribute(ref kv);
 			}
 			Proposition(out e);
 			c = new AssertCmd(x, e, kv); 
-			Expect(8);
+			Expect(9);
 			break;
 		}
-		case 47: {
+		case 48: {
 			Get();
 			x = t; 
-			while (la.kind == 27) {
+			while (la.kind == 28) {
 				Attribute(ref kv);
 			}
 			Proposition(out e);
 			c = new AssumeCmd(x, e, kv); 
-			Expect(8);
+			Expect(9);
 			break;
 		}
-		case 48: {
+		case 49: {
 			Get();
 			x = t; 
 			Idents(out xs);
-			Expect(8);
+			Expect(9);
 			ids = new List<IdentifierExpr>();
 			foreach(IToken/*!*/ y in xs){
 			 Contract.Assert(y != null);
@@ -1041,25 +1041,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 			
 			break;
 		}
-		case 35: case 51: case 52: {
+		case 36: case 52: case 53: {
 			CallCmd(out cn);
-			Expect(8);
+			Expect(9);
 			c = cn; 
 			break;
 		}
-		case 53: {
+		case 54: {
 			ParCallCmd(out cn);
 			c = cn; 
 			break;
 		}
-		case 49: {
+		case 50: {
 			Get();
 			x = t; 
-			Expect(8);
+			Expect(9);
 			c = new YieldCmd(x); 
 			break;
 		}
-		default: SynErr(105); break;
+		default: SynErr(106); break;
 		}
 	}
 
@@ -1067,16 +1067,16 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd;  Contract.Assume(cce.IsPeerConsistent(ec));
 		IfCmd/*!*/ ifcmd;  WhileCmd/*!*/ wcmd;  BreakCmd/*!*/ bcmd;
 		
-		if (la.kind == 40) {
+		if (la.kind == 41) {
 			IfCmd(out ifcmd);
 			ec = ifcmd; 
-		} else if (la.kind == 42) {
+		} else if (la.kind == 43) {
 			WhileCmd(out wcmd);
 			ec = wcmd; 
-		} else if (la.kind == 45) {
+		} else if (la.kind == 46) {
 			BreakCmd(out bcmd);
 			ec = bcmd; 
-		} else SynErr(106);
+		} else SynErr(107);
 	}
 
 	void TransferCmd(out TransferCmd/*!*/ tc) {
@@ -1084,7 +1084,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		Token y;  List<IToken>/*!*/ xs;
 		List<String> ss = new List<String>();
 		
-		if (la.kind == 38) {
+		if (la.kind == 39) {
 			Get();
 			y = t; 
 			Idents(out xs);
@@ -1093,11 +1093,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 			 ss.Add(s.val); }
 			tc = new GotoCmd(y, ss);
 			
-		} else if (la.kind == 39) {
+		} else if (la.kind == 40) {
 			Get();
 			tc = new ReturnCmd(t); 
-		} else SynErr(107);
-		Expect(8);
+		} else SynErr(108);
+		Expect(9);
 	}
 
 	void IfCmd(out IfCmd/*!*/ ifcmd) {
@@ -1107,21 +1107,21 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		IfCmd/*!*/ elseIf;  IfCmd elseIfOption = null;
 		StmtList/*!*/ els;  StmtList elseOption = null;
 		
-		Expect(40);
+		Expect(41);
 		x = t; 
 		Guard(out guard);
-		Expect(27);
+		Expect(28);
 		StmtList(out thn);
-		if (la.kind == 41) {
+		if (la.kind == 42) {
 			Get();
-			if (la.kind == 40) {
+			if (la.kind == 41) {
 				IfCmd(out elseIf);
 				elseIfOption = elseIf; 
-			} else if (la.kind == 27) {
+			} else if (la.kind == 28) {
 				Get();
 				StmtList(out els);
 				elseOption = els; 
-			} else SynErr(108);
+			} else SynErr(109);
 		}
 		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); 
 	}
@@ -1133,18 +1133,18 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		StmtList/*!*/ body;
 		QKeyValue kv = null;
 		
-		Expect(42);
+		Expect(43);
 		x = t; 
 		Guard(out guard);
 		Contract.Assume(guard == null || cce.Owner.None(guard)); 
-		while (la.kind == 35 || la.kind == 43) {
+		while (la.kind == 36 || la.kind == 44) {
 			isFree = false; z = la/*lookahead token*/; 
-			if (la.kind == 35) {
+			if (la.kind == 36) {
 				Get();
 				isFree = true;  
 			}
-			Expect(43);
-			while (la.kind == 27) {
+			Expect(44);
+			while (la.kind == 28) {
 				Attribute(ref kv);
 			}
 			Expression(out e);
@@ -1155,9 +1155,9 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 			}
 			kv = null;
 			
-			Expect(8);
+			Expect(9);
 		}
-		Expect(27);
+		Expect(28);
 		StmtList(out body);
 		wcmd = new WhileCmd(x, guard, invariants, body); 
 	}
@@ -1166,27 +1166,27 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x;  IToken/*!*/ y;
 		string breakLabel = null;
 		
-		Expect(45);
+		Expect(46);
 		x = t; 
 		if (la.kind == 1) {
 			Ident(out y);
 			breakLabel = y.val; 
 		}
-		Expect(8);
+		Expect(9);
 		bcmd = new BreakCmd(x, breakLabel); 
 	}
 
 	void Guard(out Expr e) {
 		Expr/*!*/ ee;  e = null; 
-		Expect(9);
-		if (la.kind == 44) {
+		Expect(10);
+		if (la.kind == 45) {
 			Get();
 			e = null; 
 		} else if (StartOf(9)) {
 			Expression(out ee);
 			e = ee; 
-		} else SynErr(109);
-		Expect(10);
+		} else SynErr(110);
+		Expect(11);
 	}
 
 	void LabelOrAssign(out Cmd c, out IToken label) {
@@ -1199,40 +1199,40 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		
 		Ident(out id);
 		x = t; 
-		if (la.kind == 11) {
+		if (la.kind == 12) {
 			Get();
 			c = null;  label = x; 
-		} else if (la.kind == 12 || la.kind == 17 || la.kind == 50) {
+		} else if (la.kind == 13 || la.kind == 18 || la.kind == 51) {
 			lhss = new List<AssignLhs/*!*/>(); 
 			lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); 
-			while (la.kind == 17) {
+			while (la.kind == 18) {
 				MapAssignIndex(out y, out indexes);
 				lhs = new MapAssignLhs(y, lhs, indexes); 
 			}
 			lhss.Add(lhs); 
-			while (la.kind == 12) {
+			while (la.kind == 13) {
 				Get();
 				Ident(out id);
 				lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); 
-				while (la.kind == 17) {
+				while (la.kind == 18) {
 					MapAssignIndex(out y, out indexes);
 					lhs = new MapAssignLhs(y, lhs, indexes); 
 				}
 				lhss.Add(lhs); 
 			}
-			Expect(50);
+			Expect(51);
 			x = t; /* use location of := */ 
 			Expression(out e0);
 			rhss = new List<Expr/*!*/> ();
 			rhss.Add(e0); 
-			while (la.kind == 12) {
+			while (la.kind == 13) {
 				Get();
 				Expression(out e0);
 				rhss.Add(e0); 
 			}
-			Expect(8);
+			Expect(9);
 			c = new AssignCmd(x, lhss, rhss); 
-		} else SynErr(110);
+		} else SynErr(111);
 	}
 
 	void CallCmd(out Cmd c) {
@@ -1243,17 +1243,17 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		QKeyValue kv = null;
 		c = null;
 		
-		if (la.kind == 51) {
+		if (la.kind == 52) {
 			Get();
 			isAsync = true;  
 		}
-		if (la.kind == 35) {
+		if (la.kind == 36) {
 			Get();
 			isFree = true;  
 		}
-		Expect(52);
+		Expect(53);
 		x = t; 
-		while (la.kind == 27) {
+		while (la.kind == 28) {
 			Attribute(ref kv);
 		}
 		CallParams(isAsync, isFree, kv, x, out c);
@@ -1267,19 +1267,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		Cmd c = null;
 		List<CallCmd> callCmds = new List<CallCmd>();
 		
-		Expect(53);
+		Expect(54);
 		x = t; 
-		while (la.kind == 27) {
+		while (la.kind == 28) {
 			Attribute(ref kv);
 		}
 		CallParams(false, false, kv, x, out c);
 		callCmds.Add((CallCmd)c); 
-		while (la.kind == 54) {
+		while (la.kind == 55) {
 			Get();
 			CallParams(false, false, kv, x, out c);
 			callCmds.Add((CallCmd)c); 
 		}
-		Expect(8);
+		Expect(9);
 		d = new ParCallCmd(x, callCmds, kv); 
 	}
 
@@ -1287,18 +1287,18 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List<Expr/*!*/> ();
 		Expr/*!*/ e;
 		
-		Expect(17);
+		Expect(18);
 		x = t; 
 		if (StartOf(9)) {
 			Expression(out e);
 			indexes.Add(e); 
-			while (la.kind == 12) {
+			while (la.kind == 13) {
 				Get();
 				Expression(out e);
 				indexes.Add(e); 
 			}
 		}
-		Expect(18);
+		Expect(19);
 	}
 
 	void CallParams(bool isAsync, bool isFree, QKeyValue kv, IToken x, out Cmd c) {
@@ -1310,53 +1310,53 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		c = null;
 		
 		Ident(out first);
-		if (la.kind == 9) {
+		if (la.kind == 10) {
 			Get();
 			if (StartOf(9)) {
 				Expression(out en);
 				es.Add(en); 
-				while (la.kind == 12) {
+				while (la.kind == 13) {
 					Get();
 					Expression(out en);
 					es.Add(en); 
 				}
 			}
-			Expect(10);
+			Expect(11);
 			c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; 
-		} else if (la.kind == 12 || la.kind == 50) {
+		} else if (la.kind == 13 || la.kind == 51) {
 			ids.Add(new IdentifierExpr(first, first.val)); 
-			if (la.kind == 12) {
+			if (la.kind == 13) {
 				Get();
 				Ident(out p);
 				ids.Add(new IdentifierExpr(p, p.val)); 
-				while (la.kind == 12) {
+				while (la.kind == 13) {
 					Get();
 					Ident(out p);
 					ids.Add(new IdentifierExpr(p, p.val)); 
 				}
 			}
-			Expect(50);
+			Expect(51);
 			Ident(out first);
-			Expect(9);
+			Expect(10);
 			if (StartOf(9)) {
 				Expression(out en);
 				es.Add(en); 
-				while (la.kind == 12) {
+				while (la.kind == 13) {
 					Get();
 					Expression(out en);
 					es.Add(en); 
 				}
 			}
-			Expect(10);
+			Expect(11);
 			c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; 
-		} else SynErr(111);
+		} else SynErr(112);
 	}
 
 	void Expressions(out List<Expr>/*!*/ es) {
 		Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List<Expr>(); 
 		Expression(out e);
 		es.Add(e); 
-		while (la.kind == 12) {
+		while (la.kind == 13) {
 			Get();
 			Expression(out e);
 			es.Add(e); 
@@ -1367,7 +1367,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		LogicalExpression(out e0);
 		if (StartOf(10)) {
-			if (la.kind == 57 || la.kind == 58) {
+			if (la.kind == 58 || la.kind == 59) {
 				ImpliesOp();
 				x = t; 
 				ImpliesExpression(true, out e1);
@@ -1379,7 +1379,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 				x = t; 
 				LogicalExpression(out e1);
 				e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); 
-				while (la.kind == 59 || la.kind == 60) {
+				while (la.kind == 60 || la.kind == 61) {
 					ExpliesOp();
 					x = t; 
 					LogicalExpression(out e1);
@@ -1390,23 +1390,23 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 	}
 
 	void EquivOp() {
-		if (la.kind == 55) {
+		if (la.kind == 56) {
 			Get();
-		} else if (la.kind == 56) {
+		} else if (la.kind == 57) {
 			Get();
-		} else SynErr(112);
+		} else SynErr(113);
 	}
 
 	void LogicalExpression(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		RelationalExpression(out e0);
 		if (StartOf(11)) {
-			if (la.kind == 61 || la.kind == 62) {
+			if (la.kind == 62 || la.kind == 63) {
 				AndOp();
 				x = t; 
 				RelationalExpression(out e1);
 				e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); 
-				while (la.kind == 61 || la.kind == 62) {
+				while (la.kind == 62 || la.kind == 63) {
 					AndOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1417,7 +1417,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 				x = t; 
 				RelationalExpression(out e1);
 				e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); 
-				while (la.kind == 63 || la.kind == 64) {
+				while (la.kind == 64 || la.kind == 65) {
 					OrOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1428,19 +1428,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 	}
 
 	void ImpliesOp() {
-		if (la.kind == 57) {
+		if (la.kind == 58) {
 			Get();
-		} else if (la.kind == 58) {
+		} else if (la.kind == 59) {
 			Get();
-		} else SynErr(113);
+		} else SynErr(114);
 	}
 
 	void ExpliesOp() {
-		if (la.kind == 59) {
+		if (la.kind == 60) {
 			Get();
-		} else if (la.kind == 60) {
+		} else if (la.kind == 61) {
 			Get();
-		} else SynErr(114);
+		} else SynErr(115);
 	}
 
 	void RelationalExpression(out Expr/*!*/ e0) {
@@ -1454,25 +1454,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 	}
 
 	void AndOp() {
-		if (la.kind == 61) {
+		if (la.kind == 62) {
 			Get();
-		} else if (la.kind == 62) {
+		} else if (la.kind == 63) {
 			Get();
-		} else SynErr(115);
+		} else SynErr(116);
 	}
 
 	void OrOp() {
-		if (la.kind == 63) {
+		if (la.kind == 64) {
 			Get();
-		} else if (la.kind == 64) {
+		} else if (la.kind == 65) {
 			Get();
-		} else SynErr(116);
+		} else SynErr(117);
 	}
 
 	void BvTerm(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		Term(out e0);
-		while (la.kind == 73) {
+		while (la.kind == 74) {
 			Get();
 			x = t; 
 			Term(out e1);
@@ -1483,64 +1483,64 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 	void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
 		switch (la.kind) {
-		case 65: {
+		case 66: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Eq; 
 			break;
 		}
-		case 19: {
+		case 20: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Lt; 
 			break;
 		}
-		case 20: {
+		case 21: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Gt; 
 			break;
 		}
-		case 66: {
+		case 67: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Le; 
 			break;
 		}
-		case 67: {
+		case 68: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Ge; 
 			break;
 		}
-		case 68: {
+		case 69: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Neq; 
 			break;
 		}
-		case 69: {
+		case 70: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Subtype; 
 			break;
 		}
-		case 70: {
+		case 71: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Neq; 
 			break;
 		}
-		case 71: {
+		case 72: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Le; 
 			break;
 		}
-		case 72: {
+		case 73: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Ge; 
 			break;
 		}
-		default: SynErr(117); break;
+		default: SynErr(118); break;
 		}
 	}
 
 	void Term(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; 
 		Factor(out e0);
-		while (la.kind == 74 || la.kind == 75) {
+		while (la.kind == 75 || la.kind == 76) {
 			AddOp(out x, out op);
 			Factor(out e1);
 			e0 = Expr.Binary(x, op, e0, e1); 
@@ -1559,19 +1559,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 
 	void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
-		if (la.kind == 74) {
+		if (la.kind == 75) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Add; 
-		} else if (la.kind == 75) {
+		} else if (la.kind == 76) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Sub; 
-		} else SynErr(118);
+		} else SynErr(119);
 	}
 
 	void Power(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		UnaryExpression(out e0);
-		if (la.kind == 79) {
+		if (la.kind == 80) {
 			Get();
 			x = t; 
 			Power(out e1);
@@ -1581,46 +1581,46 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 
 	void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
-		if (la.kind == 44) {
+		if (la.kind == 45) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Mul; 
-		} else if (la.kind == 76) {
+		} else if (la.kind == 77) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Div; 
-		} else if (la.kind == 77) {
+		} else if (la.kind == 78) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Mod; 
-		} else if (la.kind == 78) {
+		} else if (la.kind == 79) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.RealDiv; 
-		} else SynErr(119);
+		} else SynErr(120);
 	}
 
 	void UnaryExpression(out Expr/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
 		e = dummyExpr;
 		
-		if (la.kind == 75) {
+		if (la.kind == 76) {
 			Get();
 			x = t; 
 			UnaryExpression(out e);
 			e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); 
-		} else if (la.kind == 80 || la.kind == 81) {
+		} else if (la.kind == 81 || la.kind == 82) {
 			NegOp();
 			x = t; 
 			UnaryExpression(out e);
 			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); 
 		} else if (StartOf(14)) {
 			CoercionExpression(out e);
-		} else SynErr(120);
+		} else SynErr(121);
 	}
 
 	void NegOp() {
-		if (la.kind == 80) {
+		if (la.kind == 81) {
 			Get();
-		} else if (la.kind == 81) {
+		} else if (la.kind == 82) {
 			Get();
-		} else SynErr(121);
+		} else SynErr(122);
 	}
 
 	void CoercionExpression(out Expr/*!*/ e) {
@@ -1629,7 +1629,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		BigNum bn;
 		
 		ArrayExpression(out e);
-		while (la.kind == 11) {
+		while (la.kind == 12) {
 			Get();
 			x = t; 
 			if (StartOf(6)) {
@@ -1644,7 +1644,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 				 e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
 				}
 				
-			} else SynErr(122);
+			} else SynErr(123);
 		}
 	}
 
@@ -1655,7 +1655,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		List<Expr>/*!*/ allArgs = dummyExprSeq;
 		
 		AtomExpression(out e);
-		while (la.kind == 17) {
+		while (la.kind == 18) {
 			Get();
 			x = t; allArgs = new List<Expr> ();
 			allArgs.Add(e);
@@ -1668,7 +1668,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 					else
 					 allArgs.Add(index0);
 					
-					while (la.kind == 12) {
+					while (la.kind == 13) {
 						Get();
 						Expression(out e1);
 						if (bvExtract || e1 is BvBounds)
@@ -1676,7 +1676,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 						allArgs.Add(e1);
 						
 					}
-					if (la.kind == 50) {
+					if (la.kind == 51) {
 						Get();
 						Expression(out e1);
 						if (bvExtract || e1 is BvBounds)
@@ -1690,7 +1690,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 					allArgs.Add(e1); store = true; 
 				}
 			}
-			Expect(18);
+			Expect(19);
 			if (store)
 			 e = new NAryExpr(x, new MapStore(x, allArgs.Count - 2), allArgs);
 			else if (bvExtract)
@@ -1715,7 +1715,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 	}
 
 	void AtomExpression(out Expr/*!*/ e) {
-		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;
+		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat bf;
 		List<Expr>/*!*/ es;  List<Variable>/*!*/ ds;  Trigger trig;
 		List<TypeVariable>/*!*/ typeParams;
 		IdentifierExpr/*!*/ id;
@@ -1725,12 +1725,12 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		List<Block/*!*/>/*!*/ blocks;
 		
 		switch (la.kind) {
-		case 82: {
+		case 83: {
 			Get();
 			e = new LiteralExpr(t, false); 
 			break;
 		}
-		case 83: {
+		case 84: {
 			Get();
 			e = new LiteralExpr(t, true); 
 			break;
@@ -1745,6 +1745,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 			e = new LiteralExpr(t, bd); 
 			break;
 		}
+		case 7: {
+			Float(out bf);
+			e = new LiteralExpr(t, bf); 
+			break;
+		}
 		case 2: {
 			BvLit(out bn, out n);
 			e = new LiteralExpr(t, bn, n); 
@@ -1753,65 +1758,65 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		case 1: {
 			Ident(out x);
 			id = new IdentifierExpr(x, x.val);  e = id; 
-			if (la.kind == 9) {
+			if (la.kind == 10) {
 				Get();
 				if (StartOf(9)) {
 					Expressions(out es);
 					e = new NAryExpr(x, new FunctionCall(id), es); 
-				} else if (la.kind == 10) {
+				} else if (la.kind == 11) {
 					e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); 
-				} else SynErr(123);
-				Expect(10);
+				} else SynErr(124);
+				Expect(11);
 			}
 			break;
 		}
-		case 84: {
+		case 85: {
 			Get();
 			x = t; 
-			Expect(9);
-			Expression(out e);
 			Expect(10);
+			Expression(out e);
+			Expect(11);
 			e = new OldExpr(x, e); 
 			break;
 		}
-		case 14: {
+		case 15: {
 			Get();
 			x = t; 
-			Expect(9);
-			Expression(out e);
 			Expect(10);
+			Expression(out e);
+			Expect(11);
 			e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List<Expr>{ e }); 
 			break;
 		}
-		case 15: {
+		case 16: {
 			Get();
 			x = t; 
-			Expect(9);
-			Expression(out e);
 			Expect(10);
+			Expression(out e);
+			Expect(11);
 			e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e }); 
 			break;
 		}
-		case 9: {
+		case 10: {
 			Get();
 			if (StartOf(9)) {
 				Expression(out e);
 				if (e is BvBounds)
 				 this.SemErr("parentheses around bitvector bounds " +
 				        "are not allowed"); 
-			} else if (la.kind == 88 || la.kind == 89) {
+			} else if (la.kind == 89 || la.kind == 90) {
 				Forall();
 				x = t; 
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
 				if (typeParams.Count + ds.Count > 0)
 				 e = new ForallExpr(x, typeParams, ds, kv, trig, e); 
-			} else if (la.kind == 90 || la.kind == 91) {
+			} else if (la.kind == 91 || la.kind == 92) {
 				Exists();
 				x = t; 
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
 				if (typeParams.Count + ds.Count > 0)
 				 e = new ExistsExpr(x, typeParams, ds, kv, trig, e); 
-			} else if (la.kind == 92 || la.kind == 93) {
+			} else if (la.kind == 93 || la.kind == 94) {
 				Lambda();
 				x = t; 
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
@@ -1819,20 +1824,20 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 				 SemErr("triggers not allowed in lambda expressions");
 				if (typeParams.Count + ds.Count > 0)
 				 e = new LambdaExpr(x, typeParams, ds, kv, e); 
-			} else SynErr(124);
-			Expect(10);
+			} else SynErr(125);
+			Expect(11);
 			break;
 		}
-		case 40: {
+		case 41: {
 			IfThenElseExpression(out e);
 			break;
 		}
-		case 85: {
+		case 86: {
 			CodeExpression(out locals, out blocks);
 			e = new CodeExpr(locals, blocks); 
 			break;
 		}
-		default: SynErr(125); break;
+		default: SynErr(126); break;
 		}
 	}
 
@@ -1844,7 +1849,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		} else if (la.kind == 6) {
 			Get();
 			s = t.val; 
-		} else SynErr(126);
+		} else SynErr(127);
 		try {
 		 n = BigDec.FromString(s);
 		} catch (FormatException) {
@@ -1854,6 +1859,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		
 	}
 
+	void Float(out BigFloat n) {
+		string s = ""; 
+		Expect(7);
+		s = t.val; 
+		try {
+		 n = BigFloat.FromString(s);
+		} catch (FormatException e) {
+		 this.SemErr("incorrectly formatted floating point: " + e.Message);
+		 n = BigFloat.ZERO;
+		}
+		
+	}
+
 	void BvLit(out BigNum n, out int m) {
 		Expect(2);
 		int pos = t.val.IndexOf("bv");
@@ -1871,11 +1889,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 	}
 
 	void Forall() {
-		if (la.kind == 88) {
+		if (la.kind == 89) {
 			Get();
-		} else if (la.kind == 89) {
+		} else if (la.kind == 90) {
 			Get();
-		} else SynErr(127);
+		} else SynErr(128);
 	}
 
 	void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,
@@ -1886,35 +1904,35 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		kv = null;
 		ds = new List<Variable> ();
 		
-		if (la.kind == 19) {
+		if (la.kind == 20) {
 			TypeParams(out tok, out typeParams);
-			if (la.kind == 1 || la.kind == 27) {
+			if (la.kind == 1 || la.kind == 28) {
 				BoundVars(q, out ds);
 			}
-		} else if (la.kind == 1 || la.kind == 27) {
+		} else if (la.kind == 1 || la.kind == 28) {
 			BoundVars(q, out ds);
-		} else SynErr(128);
+		} else SynErr(129);
 		QSep();
-		while (la.kind == 27) {
+		while (la.kind == 28) {
 			AttributeOrTrigger(ref kv, ref trig);
 		}
 		Expression(out body);
 	}
 
 	void Exists() {
-		if (la.kind == 90) {
+		if (la.kind == 91) {
 			Get();
-		} else if (la.kind == 91) {
+		} else if (la.kind == 92) {
 			Get();
-		} else SynErr(129);
+		} else SynErr(130);
 	}
 
 	void Lambda() {
-		if (la.kind == 92) {
+		if (la.kind == 93) {
 			Get();
-		} else if (la.kind == 93) {
+		} else if (la.kind == 94) {
 			Get();
-		} else SynErr(130);
+		} else SynErr(131);
 	}
 
 	void IfThenElseExpression(out Expr/*!*/ e) {
@@ -1922,12 +1940,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		IToken/*!*/ tok;
 		Expr/*!*/ e0, e1, e2;
 		e = dummyExpr; 
-		Expect(40);
+		Expect(41);
 		tok = t; 
 		Expression(out e0);
-		Expect(87);
+		Expect(88);
 		Expression(out e1);
-		Expect(41);
+		Expect(42);
 		Expression(out e2);
 		e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>{ e0, e1, e2 }); 
 	}
@@ -1936,8 +1954,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List<Variable>(); Block/*!*/ b;
 		blocks = new List<Block/*!*/>();
 		
-		Expect(85);
-		while (la.kind == 7) {
+		Expect(86);
+		while (la.kind == 8) {
 			LocalVars(locals);
 		}
 		SpecBlock(out b);
@@ -1946,7 +1964,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 			SpecBlock(out b);
 			blocks.Add(b); 
 		}
-		Expect(86);
+		Expect(87);
 	}
 
 	void SpecBlock(out Block/*!*/ b) {
@@ -1959,7 +1977,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		Expr/*!*/ e;
 		
 		Ident(out x);
-		Expect(11);
+		Expect(12);
 		while (StartOf(8)) {
 			LabelOrCmd(out c, out label);
 			if (c != null) {
@@ -1971,7 +1989,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 			}
 			
 		}
-		if (la.kind == 38) {
+		if (la.kind == 39) {
 			Get();
 			y = t; 
 			Idents(out xs);
@@ -1980,12 +1998,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 			 ss.Add(s.val); }
 			b = new Block(x,x.val,cs,new GotoCmd(y,ss));
 			
-		} else if (la.kind == 39) {
+		} else if (la.kind == 40) {
 			Get();
 			Expression(out e);
 			b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); 
-		} else SynErr(131);
-		Expect(8);
+		} else SynErr(132);
+		Expect(9);
 	}
 
 	void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
@@ -1993,16 +2011,16 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		string key;
 		List<object/*!*/> parameters;  object/*!*/ param;
 		
-		Expect(27);
+		Expect(28);
 		tok = t; 
-		if (la.kind == 11) {
+		if (la.kind == 12) {
 			Get();
 			Expect(1);
 			key = t.val;  parameters = new List<object/*!*/>(); 
 			if (StartOf(16)) {
 				AttributeParameter(out param);
 				parameters.Add(param); 
-				while (la.kind == 12) {
+				while (la.kind == 13) {
 					Get();
 					AttributeParameter(out param);
 					parameters.Add(param); 
@@ -2030,7 +2048,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		} else if (StartOf(9)) {
 			Expression(out e);
 			es = new List<Expr> { e }; 
-			while (la.kind == 12) {
+			while (la.kind == 13) {
 				Get();
 				Expression(out e);
 				es.Add(e); 
@@ -2041,8 +2059,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 			 trig.AddLast(new Trigger(tok, true, es, null));
 			}
 			
-		} else SynErr(132);
-		Expect(28);
+		} else SynErr(133);
+		Expect(29);
 	}
 
 	void AttributeParameter(out object/*!*/ o) {
@@ -2056,15 +2074,15 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		} else if (StartOf(9)) {
 			Expression(out e);
 			o = e; 
-		} else SynErr(133);
+		} else SynErr(134);
 	}
 
 	void QSep() {
-		if (la.kind == 94) {
+		if (la.kind == 95) {
 			Get();
-		} else if (la.kind == 95) {
+		} else if (la.kind == 96) {
 			Get();
-		} else SynErr(134);
+		} else SynErr(135);
 	}
 
 
@@ -2080,23 +2098,23 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 	}
 
 	static readonly bool[,]/*!*/ set = {
-		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
-		{x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}
+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,T, x,x,T,T, T,T,T,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,T,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,T,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,T,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,T,T,T, T,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x}
 
 	};
 } // end Parser
@@ -2127,135 +2145,136 @@ public class Errors {
 			case 3: s = "digits expected"; break;
 			case 4: s = "string expected"; break;
 			case 5: s = "decimal expected"; break;
-			case 6: s = "float expected"; break;
-			case 7: s = "\"var\" expected"; break;
-			case 8: s = "\";\" expected"; break;
-			case 9: s = "\"(\" expected"; break;
-			case 10: s = "\")\" expected"; break;
-			case 11: s = "\":\" expected"; break;
-			case 12: s = "\",\" expected"; break;
-			case 13: s = "\"where\" expected"; break;
-			case 14: s = "\"int\" expected"; break;
-			case 15: s = "\"real\" expected"; break;
-			case 16: s = "\"bool\" expected"; break;
-			case 17: s = "\"[\" expected"; break;
-			case 18: s = "\"]\" expected"; break;
-			case 19: s = "\"<\" expected"; break;
-			case 20: s = "\">\" expected"; break;
-			case 21: s = "\"const\" expected"; break;
-			case 22: s = "\"unique\" expected"; break;
-			case 23: s = "\"extends\" expected"; break;
-			case 24: s = "\"complete\" expected"; break;
-			case 25: s = "\"function\" expected"; break;
-			case 26: s = "\"returns\" expected"; break;
-			case 27: s = "\"{\" expected"; break;
-			case 28: s = "\"}\" expected"; break;
-			case 29: s = "\"axiom\" expected"; break;
-			case 30: s = "\"type\" expected"; break;
-			case 31: s = "\"=\" expected"; break;
-			case 32: s = "\"procedure\" expected"; break;
-			case 33: s = "\"implementation\" expected"; break;
-			case 34: s = "\"modifies\" expected"; break;
-			case 35: s = "\"free\" expected"; break;
-			case 36: s = "\"requires\" expected"; break;
-			case 37: s = "\"ensures\" expected"; break;
-			case 38: s = "\"goto\" expected"; break;
-			case 39: s = "\"return\" expected"; break;
-			case 40: s = "\"if\" expected"; break;
-			case 41: s = "\"else\" expected"; break;
-			case 42: s = "\"while\" expected"; break;
-			case 43: s = "\"invariant\" expected"; break;
-			case 44: s = "\"*\" expected"; break;
-			case 45: s = "\"break\" expected"; break;
-			case 46: s = "\"assert\" expected"; break;
-			case 47: s = "\"assume\" expected"; break;
-			case 48: s = "\"havoc\" expected"; break;
-			case 49: s = "\"yield\" expected"; break;
-			case 50: s = "\":=\" expected"; break;
-			case 51: s = "\"async\" expected"; break;
-			case 52: s = "\"call\" expected"; break;
-			case 53: s = "\"par\" expected"; break;
-			case 54: s = "\"|\" expected"; break;
-			case 55: s = "\"<==>\" expected"; break;
-			case 56: s = "\"\\u21d4\" expected"; break;
-			case 57: s = "\"==>\" expected"; break;
-			case 58: s = "\"\\u21d2\" expected"; break;
-			case 59: s = "\"<==\" expected"; break;
-			case 60: s = "\"\\u21d0\" expected"; break;
-			case 61: s = "\"&&\" expected"; break;
-			case 62: s = "\"\\u2227\" expected"; break;
-			case 63: s = "\"||\" expected"; break;
-			case 64: s = "\"\\u2228\" expected"; break;
-			case 65: s = "\"==\" expected"; break;
-			case 66: s = "\"<=\" expected"; break;
-			case 67: s = "\">=\" expected"; break;
-			case 68: s = "\"!=\" expected"; break;
-			case 69: s = "\"<:\" expected"; break;
-			case 70: s = "\"\\u2260\" expected"; break;
-			case 71: s = "\"\\u2264\" expected"; break;
-			case 72: s = "\"\\u2265\" expected"; break;
-			case 73: s = "\"++\" expected"; break;
-			case 74: s = "\"+\" expected"; break;
-			case 75: s = "\"-\" expected"; break;
-			case 76: s = "\"div\" expected"; break;
-			case 77: s = "\"mod\" expected"; break;
-			case 78: s = "\"/\" expected"; break;
-			case 79: s = "\"**\" expected"; break;
-			case 80: s = "\"!\" expected"; break;
-			case 81: s = "\"\\u00ac\" expected"; break;
-			case 82: s = "\"false\" expected"; break;
-			case 83: s = "\"true\" expected"; break;
-			case 84: s = "\"old\" expected"; break;
-			case 85: s = "\"|{\" expected"; break;
-			case 86: s = "\"}|\" expected"; break;
-			case 87: s = "\"then\" expected"; break;
-			case 88: s = "\"forall\" expected"; break;
-			case 89: s = "\"\\u2200\" expected"; break;
-			case 90: s = "\"exists\" expected"; break;
-			case 91: s = "\"\\u2203\" expected"; break;
-			case 92: s = "\"lambda\" expected"; break;
-			case 93: s = "\"\\u03bb\" expected"; break;
-			case 94: s = "\"::\" expected"; break;
-			case 95: s = "\"\\u2022\" expected"; break;
-			case 96: s = "??? expected"; break;
-			case 97: s = "invalid Function"; break;
+			case 6: s = "dec_float expected"; break;
+			case 7: s = "float expected"; break;
+			case 8: s = "\"var\" expected"; break;
+			case 9: s = "\";\" expected"; break;
+			case 10: s = "\"(\" expected"; break;
+			case 11: s = "\")\" expected"; break;
+			case 12: s = "\":\" expected"; break;
+			case 13: s = "\",\" expected"; break;
+			case 14: s = "\"where\" expected"; break;
+			case 15: s = "\"int\" expected"; break;
+			case 16: s = "\"real\" expected"; break;
+			case 17: s = "\"bool\" expected"; break;
+			case 18: s = "\"[\" expected"; break;
+			case 19: s = "\"]\" expected"; break;
+			case 20: s = "\"<\" expected"; break;
+			case 21: s = "\">\" expected"; break;
+			case 22: s = "\"const\" expected"; break;
+			case 23: s = "\"unique\" expected"; break;
+			case 24: s = "\"extends\" expected"; break;
+			case 25: s = "\"complete\" expected"; break;
+			case 26: s = "\"function\" expected"; break;
+			case 27: s = "\"returns\" expected"; break;
+			case 28: s = "\"{\" expected"; break;
+			case 29: s = "\"}\" expected"; break;
+			case 30: s = "\"axiom\" expected"; break;
+			case 31: s = "\"type\" expected"; break;
+			case 32: s = "\"=\" expected"; break;
+			case 33: s = "\"procedure\" expected"; break;
+			case 34: s = "\"implementation\" expected"; break;
+			case 35: s = "\"modifies\" expected"; break;
+			case 36: s = "\"free\" expected"; break;
+			case 37: s = "\"requires\" expected"; break;
+			case 38: s = "\"ensures\" expected"; break;
+			case 39: s = "\"goto\" expected"; break;
+			case 40: s = "\"return\" expected"; break;
+			case 41: s = "\"if\" expected"; break;
+			case 42: s = "\"else\" expected"; break;
+			case 43: s = "\"while\" expected"; break;
+			case 44: s = "\"invariant\" expected"; break;
+			case 45: s = "\"*\" expected"; break;
+			case 46: s = "\"break\" expected"; break;
+			case 47: s = "\"assert\" expected"; break;
+			case 48: s = "\"assume\" expected"; break;
+			case 49: s = "\"havoc\" expected"; break;
+			case 50: s = "\"yield\" expected"; break;
+			case 51: s = "\":=\" expected"; break;
+			case 52: s = "\"async\" expected"; break;
+			case 53: s = "\"call\" expected"; break;
+			case 54: s = "\"par\" expected"; break;
+			case 55: s = "\"|\" expected"; break;
+			case 56: s = "\"<==>\" expected"; break;
+			case 57: s = "\"\\u21d4\" expected"; break;
+			case 58: s = "\"==>\" expected"; break;
+			case 59: s = "\"\\u21d2\" expected"; break;
+			case 60: s = "\"<==\" expected"; break;
+			case 61: s = "\"\\u21d0\" expected"; break;
+			case 62: s = "\"&&\" expected"; break;
+			case 63: s = "\"\\u2227\" expected"; break;
+			case 64: s = "\"||\" expected"; break;
+			case 65: s = "\"\\u2228\" expected"; break;
+			case 66: s = "\"==\" expected"; break;
+			case 67: s = "\"<=\" expected"; break;
+			case 68: s = "\">=\" expected"; break;
+			case 69: s = "\"!=\" expected"; break;
+			case 70: s = "\"<:\" expected"; break;
+			case 71: s = "\"\\u2260\" expected"; break;
+			case 72: s = "\"\\u2264\" expected"; break;
+			case 73: s = "\"\\u2265\" expected"; break;
+			case 74: s = "\"++\" expected"; break;
+			case 75: s = "\"+\" expected"; break;
+			case 76: s = "\"-\" expected"; break;
+			case 77: s = "\"div\" expected"; break;
+			case 78: s = "\"mod\" expected"; break;
+			case 79: s = "\"/\" expected"; break;
+			case 80: s = "\"**\" expected"; break;
+			case 81: s = "\"!\" expected"; break;
+			case 82: s = "\"\\u00ac\" expected"; break;
+			case 83: s = "\"false\" expected"; break;
+			case 84: s = "\"true\" expected"; break;
+			case 85: s = "\"old\" expected"; break;
+			case 86: s = "\"|{\" expected"; break;
+			case 87: s = "\"}|\" expected"; break;
+			case 88: s = "\"then\" expected"; break;
+			case 89: s = "\"forall\" expected"; break;
+			case 90: s = "\"\\u2200\" expected"; break;
+			case 91: s = "\"exists\" expected"; break;
+			case 92: s = "\"\\u2203\" expected"; break;
+			case 93: s = "\"lambda\" expected"; break;
+			case 94: s = "\"\\u03bb\" expected"; break;
+			case 95: s = "\"::\" expected"; break;
+			case 96: s = "\"\\u2022\" expected"; break;
+			case 97: s = "??? expected"; break;
 			case 98: s = "invalid Function"; break;
-			case 99: s = "invalid Procedure"; break;
-			case 100: s = "invalid Type"; break;
-			case 101: s = "invalid TypeAtom"; break;
-			case 102: s = "invalid TypeArgs"; break;
-			case 103: s = "invalid Spec"; break;
-			case 104: s = "invalid SpecPrePost"; break;
-			case 105: s = "invalid LabelOrCmd"; break;
-			case 106: s = "invalid StructuredCmd"; break;
-			case 107: s = "invalid TransferCmd"; break;
-			case 108: s = "invalid IfCmd"; break;
-			case 109: s = "invalid Guard"; break;
-			case 110: s = "invalid LabelOrAssign"; break;
-			case 111: s = "invalid CallParams"; break;
-			case 112: s = "invalid EquivOp"; break;
-			case 113: s = "invalid ImpliesOp"; break;
-			case 114: s = "invalid ExpliesOp"; break;
-			case 115: s = "invalid AndOp"; break;
-			case 116: s = "invalid OrOp"; break;
-			case 117: s = "invalid RelOp"; break;
-			case 118: s = "invalid AddOp"; break;
-			case 119: s = "invalid MulOp"; break;
-			case 120: s = "invalid UnaryExpression"; break;
-			case 121: s = "invalid NegOp"; break;
-			case 122: s = "invalid CoercionExpression"; break;
-			case 123: s = "invalid AtomExpression"; break;
+			case 99: s = "invalid Function"; break;
+			case 100: s = "invalid Procedure"; break;
+			case 101: s = "invalid Type"; break;
+			case 102: s = "invalid TypeAtom"; break;
+			case 103: s = "invalid TypeArgs"; break;
+			case 104: s = "invalid Spec"; break;
+			case 105: s = "invalid SpecPrePost"; break;
+			case 106: s = "invalid LabelOrCmd"; break;
+			case 107: s = "invalid StructuredCmd"; break;
+			case 108: s = "invalid TransferCmd"; break;
+			case 109: s = "invalid IfCmd"; break;
+			case 110: s = "invalid Guard"; break;
+			case 111: s = "invalid LabelOrAssign"; break;
+			case 112: s = "invalid CallParams"; break;
+			case 113: s = "invalid EquivOp"; break;
+			case 114: s = "invalid ImpliesOp"; break;
+			case 115: s = "invalid ExpliesOp"; break;
+			case 116: s = "invalid AndOp"; break;
+			case 117: s = "invalid OrOp"; break;
+			case 118: s = "invalid RelOp"; break;
+			case 119: s = "invalid AddOp"; break;
+			case 120: s = "invalid MulOp"; break;
+			case 121: s = "invalid UnaryExpression"; break;
+			case 122: s = "invalid NegOp"; break;
+			case 123: s = "invalid CoercionExpression"; break;
 			case 124: s = "invalid AtomExpression"; break;
 			case 125: s = "invalid AtomExpression"; break;
-			case 126: s = "invalid Dec"; break;
-			case 127: s = "invalid Forall"; break;
-			case 128: s = "invalid QuantifierBody"; break;
-			case 129: s = "invalid Exists"; break;
-			case 130: s = "invalid Lambda"; break;
-			case 131: s = "invalid SpecBlock"; break;
-			case 132: s = "invalid AttributeOrTrigger"; break;
-			case 133: s = "invalid AttributeParameter"; break;
-			case 134: s = "invalid QSep"; break;
+			case 126: s = "invalid AtomExpression"; break;
+			case 127: s = "invalid Dec"; break;
+			case 128: s = "invalid Forall"; break;
+			case 129: s = "invalid QuantifierBody"; break;
+			case 130: s = "invalid Exists"; break;
+			case 131: s = "invalid Lambda"; break;
+			case 132: s = "invalid SpecBlock"; break;
+			case 133: s = "invalid AttributeOrTrigger"; break;
+			case 134: s = "invalid AttributeParameter"; break;
+			case 135: s = "invalid QSep"; break;
 
 			default: s = "error " + n; break;
 		}
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index e068fc4b..1185963f 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
 public class Scanner {
 	const char EOL = '\n';
 	const int eofSym = 0; /* pdt */
-	const int maxT = 96;
-	const int noSym = 96;
+	const int maxT = 97;
+	const int noSym = 97;
 
 
 	[ContractInvariantMethod]
@@ -267,41 +267,41 @@ public class Scanner {
 		for (int i = 65; i <= 90; ++i) start[i] = 2;
 		for (int i = 94; i <= 122; ++i) start[i] = 2;
 		for (int i = 126; i <= 126; ++i) start[i] = 2;
-		for (int i = 48; i <= 57; ++i) start[i] = 16;
+		for (int i = 48; i <= 57; ++i) start[i] = 19;
 		for (int i = 34; i <= 34; ++i) start[i] = 6;
 		start[92] = 1; 
-		start[59] = 19; 
-		start[40] = 20; 
-		start[41] = 21; 
-		start[58] = 55; 
-		start[44] = 22; 
-		start[91] = 23; 
-		start[93] = 24; 
-		start[60] = 56; 
-		start[62] = 57; 
-		start[123] = 25; 
-		start[125] = 58; 
-		start[61] = 59; 
-		start[42] = 60; 
-		start[124] = 61; 
-		start[8660] = 28; 
-		start[8658] = 30; 
-		start[8656] = 31; 
-		start[38] = 32; 
-		start[8743] = 34; 
-		start[8744] = 36; 
-		start[33] = 62; 
-		start[8800] = 40; 
-		start[8804] = 41; 
-		start[8805] = 42; 
-		start[43] = 63; 
-		start[45] = 44; 
-		start[47] = 45; 
-		start[172] = 47; 
-		start[8704] = 50; 
-		start[8707] = 51; 
-		start[955] = 52; 
-		start[8226] = 54; 
+		start[59] = 24; 
+		start[40] = 25; 
+		start[41] = 26; 
+		start[58] = 60; 
+		start[44] = 27; 
+		start[91] = 28; 
+		start[93] = 29; 
+		start[60] = 61; 
+		start[62] = 62; 
+		start[123] = 30; 
+		start[125] = 63; 
+		start[61] = 64; 
+		start[42] = 65; 
+		start[124] = 66; 
+		start[8660] = 33; 
+		start[8658] = 35; 
+		start[8656] = 36; 
+		start[38] = 37; 
+		start[8743] = 39; 
+		start[8744] = 41; 
+		start[33] = 67; 
+		start[8800] = 45; 
+		start[8804] = 46; 
+		start[8805] = 47; 
+		start[43] = 68; 
+		start[45] = 49; 
+		start[47] = 50; 
+		start[172] = 52; 
+		start[8704] = 55; 
+		start[8707] = 56; 
+		start[955] = 57; 
+		start[8226] = 59; 
 		start[Buffer.EOF] = -1;
 
 	}
@@ -503,48 +503,48 @@ public class Scanner {
 
 	void CheckLiteral() {
 		switch (t.val) {
-			case "var": t.kind = 7; break;
-			case "where": t.kind = 13; break;
-			case "int": t.kind = 14; break;
-			case "real": t.kind = 15; break;
-			case "bool": t.kind = 16; break;
-			case "const": t.kind = 21; break;
-			case "unique": t.kind = 22; break;
-			case "extends": t.kind = 23; break;
-			case "complete": t.kind = 24; break;
-			case "function": t.kind = 25; break;
-			case "returns": t.kind = 26; break;
-			case "axiom": t.kind = 29; break;
-			case "type": t.kind = 30; break;
-			case "procedure": t.kind = 32; break;
-			case "implementation": t.kind = 33; break;
-			case "modifies": t.kind = 34; break;
-			case "free": t.kind = 35; break;
-			case "requires": t.kind = 36; break;
-			case "ensures": t.kind = 37; break;
-			case "goto": t.kind = 38; break;
-			case "return": t.kind = 39; break;
-			case "if": t.kind = 40; break;
-			case "else": t.kind = 41; break;
-			case "while": t.kind = 42; break;
-			case "invariant": t.kind = 43; break;
-			case "break": t.kind = 45; break;
-			case "assert": t.kind = 46; break;
-			case "assume": t.kind = 47; break;
-			case "havoc": t.kind = 48; break;
-			case "yield": t.kind = 49; break;
-			case "async": t.kind = 51; break;
-			case "call": t.kind = 52; break;
-			case "par": t.kind = 53; break;
-			case "div": t.kind = 76; break;
-			case "mod": t.kind = 77; break;
-			case "false": t.kind = 82; break;
-			case "true": t.kind = 83; break;
-			case "old": t.kind = 84; break;
-			case "then": t.kind = 87; break;
-			case "forall": t.kind = 88; break;
-			case "exists": t.kind = 90; break;
-			case "lambda": t.kind = 92; break;
+			case "var": t.kind = 8; break;
+			case "where": t.kind = 14; break;
+			case "int": t.kind = 15; break;
+			case "real": t.kind = 16; break;
+			case "bool": t.kind = 17; break;
+			case "const": t.kind = 22; break;
+			case "unique": t.kind = 23; break;
+			case "extends": t.kind = 24; break;
+			case "complete": t.kind = 25; break;
+			case "function": t.kind = 26; break;
+			case "returns": t.kind = 27; break;
+			case "axiom": t.kind = 30; break;
+			case "type": t.kind = 31; break;
+			case "procedure": t.kind = 33; break;
+			case "implementation": t.kind = 34; break;
+			case "modifies": t.kind = 35; break;
+			case "free": t.kind = 36; break;
+			case "requires": t.kind = 37; break;
+			case "ensures": t.kind = 38; break;
+			case "goto": t.kind = 39; break;
+			case "return": t.kind = 40; break;
+			case "if": t.kind = 41; break;
+			case "else": t.kind = 42; break;
+			case "while": t.kind = 43; break;
+			case "invariant": t.kind = 44; break;
+			case "break": t.kind = 46; break;
+			case "assert": t.kind = 47; break;
+			case "assume": t.kind = 48; break;
+			case "havoc": t.kind = 49; break;
+			case "yield": t.kind = 50; break;
+			case "async": t.kind = 52; break;
+			case "call": t.kind = 53; break;
+			case "par": t.kind = 54; break;
+			case "div": t.kind = 77; break;
+			case "mod": t.kind = 78; break;
+			case "false": t.kind = 83; break;
+			case "true": t.kind = 84; break;
+			case "old": t.kind = 85; break;
+			case "then": t.kind = 88; break;
+			case "forall": t.kind = 89; break;
+			case "exists": t.kind = 91; break;
+			case "lambda": t.kind = 93; break;
 			default: break;
 		}
 	}
@@ -597,182 +597,201 @@ public class Scanner {
 			case 6:
 				if (ch == '"') {AddCh(); goto case 7;}
 				else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
-				else if (ch == 92) {AddCh(); goto case 17;}
+				else if (ch == 92) {AddCh(); goto case 20;}
 				else {goto case 0;}
 			case 7:
 				{t.kind = 4; break;}
 			case 8:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
-				else if (ch == '-') {AddCh(); goto case 9;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
 				else {goto case 0;}
 			case 9:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
-				else {goto case 0;}
-			case 10:
 				recEnd = pos; recKind = 5;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
 				else {t.kind = 5; break;}
-			case 11:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+			case 10:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;}
 				else {goto case 0;}
-			case 12:
+			case 11:
 				recEnd = pos; recKind = 6;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
-				else if (ch == 'e') {AddCh(); goto case 13;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;}
+				else if (ch == 'e') {AddCh(); goto case 12;}
 				else {t.kind = 6; break;}
+			case 12:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
+				else if (ch == '-') {AddCh(); goto case 13;}
+				else {goto case 0;}
 			case 13:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
-				else if (ch == '-') {AddCh(); goto case 14;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
 				else {goto case 0;}
 			case 14:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
-				else {goto case 0;}
-			case 15:
 				recEnd = pos; recKind = 6;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
 				else {t.kind = 6; break;}
+			case 15:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
+				else {goto case 0;}
 			case 16:
-				recEnd = pos; recKind = 3;
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
+				else if (ch == 'e') {AddCh(); goto case 17;}
+				else {goto case 0;}
+			case 17:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
+				else {goto case 0;}
+			case 18:
+				recEnd = pos; recKind = 7;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
+				else {t.kind = 7; break;}
+			case 19:
+				recEnd = pos; recKind = 3;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 19;}
 				else if (ch == 'b') {AddCh(); goto case 3;}
-				else if (ch == 'e') {AddCh(); goto case 8;}
-				else if (ch == '.') {AddCh(); goto case 11;}
+				else if (ch == 'e') {AddCh(); goto case 21;}
+				else if (ch == '.') {AddCh(); goto case 10;}
 				else {t.kind = 3; break;}
-			case 17:
-				if (ch == '"') {AddCh(); goto case 18;}
+			case 20:
+				if (ch == '"') {AddCh(); goto case 22;}
 				else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
-				else if (ch == 92) {AddCh(); goto case 17;}
+				else if (ch == 92) {AddCh(); goto case 20;}
 				else {goto case 0;}
-			case 18:
+			case 21:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;}
+				else if (ch == '-') {AddCh(); goto case 8;}
+				else {goto case 0;}
+			case 22:
 				recEnd = pos; recKind = 4;
 				if (ch == '"') {AddCh(); goto case 7;}
 				else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
-				else if (ch == 92) {AddCh(); goto case 17;}
+				else if (ch == 92) {AddCh(); goto case 20;}
 				else {t.kind = 4; break;}
-			case 19:
-				{t.kind = 8; break;}
-			case 20:
-				{t.kind = 9; break;}
-			case 21:
-				{t.kind = 10; break;}
-			case 22:
-				{t.kind = 12; break;}
 			case 23:
-				{t.kind = 17; break;}
+				recEnd = pos; recKind = 5;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;}
+				else if (ch == 'f') {AddCh(); goto case 15;}
+				else {t.kind = 5; break;}
 			case 24:
-				{t.kind = 18; break;}
+				{t.kind = 9; break;}
 			case 25:
-				{t.kind = 27; break;}
+				{t.kind = 10; break;}
 			case 26:
-				{t.kind = 50; break;}
+				{t.kind = 11; break;}
 			case 27:
-				{t.kind = 55; break;}
+				{t.kind = 13; break;}
 			case 28:
-				{t.kind = 56; break;}
+				{t.kind = 18; break;}
 			case 29:
-				{t.kind = 57; break;}
+				{t.kind = 19; break;}
 			case 30:
-				{t.kind = 58; break;}
+				{t.kind = 28; break;}
 			case 31:
-				{t.kind = 60; break;}
+				{t.kind = 51; break;}
 			case 32:
-				if (ch == '&') {AddCh(); goto case 33;}
-				else {goto case 0;}
+				{t.kind = 56; break;}
 			case 33:
-				{t.kind = 61; break;}
+				{t.kind = 57; break;}
 			case 34:
-				{t.kind = 62; break;}
+				{t.kind = 58; break;}
 			case 35:
-				{t.kind = 63; break;}
+				{t.kind = 59; break;}
 			case 36:
-				{t.kind = 64; break;}
+				{t.kind = 61; break;}
 			case 37:
-				{t.kind = 67; break;}
+				if (ch == '&') {AddCh(); goto case 38;}
+				else {goto case 0;}
 			case 38:
-				{t.kind = 68; break;}
+				{t.kind = 62; break;}
 			case 39:
-				{t.kind = 69; break;}
+				{t.kind = 63; break;}
 			case 40:
-				{t.kind = 70; break;}
+				{t.kind = 64; break;}
 			case 41:
-				{t.kind = 71; break;}
+				{t.kind = 65; break;}
 			case 42:
-				{t.kind = 72; break;}
+				{t.kind = 68; break;}
 			case 43:
-				{t.kind = 73; break;}
+				{t.kind = 69; break;}
 			case 44:
-				{t.kind = 75; break;}
+				{t.kind = 70; break;}
 			case 45:
-				{t.kind = 78; break;}
+				{t.kind = 71; break;}
 			case 46:
-				{t.kind = 79; break;}
+				{t.kind = 72; break;}
 			case 47:
-				{t.kind = 81; break;}
+				{t.kind = 73; break;}
 			case 48:
-				{t.kind = 85; break;}
+				{t.kind = 74; break;}
 			case 49:
-				{t.kind = 86; break;}
+				{t.kind = 76; break;}
 			case 50:
-				{t.kind = 89; break;}
+				{t.kind = 79; break;}
 			case 51:
-				{t.kind = 91; break;}
+				{t.kind = 80; break;}
 			case 52:
-				{t.kind = 93; break;}
+				{t.kind = 82; break;}
 			case 53:
-				{t.kind = 94; break;}
+				{t.kind = 86; break;}
 			case 54:
-				{t.kind = 95; break;}
+				{t.kind = 87; break;}
 			case 55:
-				recEnd = pos; recKind = 11;
-				if (ch == '=') {AddCh(); goto case 26;}
-				else if (ch == ':') {AddCh(); goto case 53;}
-				else {t.kind = 11; break;}
+				{t.kind = 90; break;}
 			case 56:
-				recEnd = pos; recKind = 19;
-				if (ch == '=') {AddCh(); goto case 64;}
-				else if (ch == ':') {AddCh(); goto case 39;}
-				else {t.kind = 19; break;}
+				{t.kind = 92; break;}
 			case 57:
-				recEnd = pos; recKind = 20;
-				if (ch == '=') {AddCh(); goto case 37;}
-				else {t.kind = 20; break;}
+				{t.kind = 94; break;}
 			case 58:
-				recEnd = pos; recKind = 28;
-				if (ch == '|') {AddCh(); goto case 49;}
-				else {t.kind = 28; break;}
+				{t.kind = 95; break;}
 			case 59:
-				recEnd = pos; recKind = 31;
-				if (ch == '=') {AddCh(); goto case 65;}
-				else {t.kind = 31; break;}
+				{t.kind = 96; break;}
 			case 60:
-				recEnd = pos; recKind = 44;
-				if (ch == '*') {AddCh(); goto case 46;}
-				else {t.kind = 44; break;}
+				recEnd = pos; recKind = 12;
+				if (ch == '=') {AddCh(); goto case 31;}
+				else if (ch == ':') {AddCh(); goto case 58;}
+				else {t.kind = 12; break;}
 			case 61:
-				recEnd = pos; recKind = 54;
-				if (ch == '|') {AddCh(); goto case 35;}
-				else if (ch == '{') {AddCh(); goto case 48;}
-				else {t.kind = 54; break;}
+				recEnd = pos; recKind = 20;
+				if (ch == '=') {AddCh(); goto case 69;}
+				else if (ch == ':') {AddCh(); goto case 44;}
+				else {t.kind = 20; break;}
 			case 62:
-				recEnd = pos; recKind = 80;
-				if (ch == '=') {AddCh(); goto case 38;}
-				else {t.kind = 80; break;}
+				recEnd = pos; recKind = 21;
+				if (ch == '=') {AddCh(); goto case 42;}
+				else {t.kind = 21; break;}
 			case 63:
-				recEnd = pos; recKind = 74;
-				if (ch == '+') {AddCh(); goto case 43;}
-				else {t.kind = 74; break;}
+				recEnd = pos; recKind = 29;
+				if (ch == '|') {AddCh(); goto case 54;}
+				else {t.kind = 29; break;}
 			case 64:
-				recEnd = pos; recKind = 66;
-				if (ch == '=') {AddCh(); goto case 66;}
-				else {t.kind = 66; break;}
+				recEnd = pos; recKind = 32;
+				if (ch == '=') {AddCh(); goto case 70;}
+				else {t.kind = 32; break;}
 			case 65:
-				recEnd = pos; recKind = 65;
-				if (ch == '>') {AddCh(); goto case 29;}
-				else {t.kind = 65; break;}
+				recEnd = pos; recKind = 45;
+				if (ch == '*') {AddCh(); goto case 51;}
+				else {t.kind = 45; break;}
 			case 66:
-				recEnd = pos; recKind = 59;
-				if (ch == '>') {AddCh(); goto case 27;}
-				else {t.kind = 59; break;}
+				recEnd = pos; recKind = 55;
+				if (ch == '|') {AddCh(); goto case 40;}
+				else if (ch == '{') {AddCh(); goto case 53;}
+				else {t.kind = 55; break;}
+			case 67:
+				recEnd = pos; recKind = 81;
+				if (ch == '=') {AddCh(); goto case 43;}
+				else {t.kind = 81; break;}
+			case 68:
+				recEnd = pos; recKind = 75;
+				if (ch == '+') {AddCh(); goto case 48;}
+				else {t.kind = 75; break;}
+			case 69:
+				recEnd = pos; recKind = 67;
+				if (ch == '=') {AddCh(); goto case 71;}
+				else {t.kind = 67; break;}
+			case 70:
+				recEnd = pos; recKind = 66;
+				if (ch == '>') {AddCh(); goto case 34;}
+				else {t.kind = 66; break;}
+			case 71:
+				recEnd = pos; recKind = 60;
+				if (ch == '>') {AddCh(); goto case 32;}
+				else {t.kind = 60; break;}
 
 		}
 		t.val = new String(tval, 0, tlen);
diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl
index 1a642835..d7faa4b0 100644
--- a/Test/floats/float0.bpl
+++ b/Test/floats/float0.bpl
@@ -4,11 +4,11 @@ procedure foo(x : real) returns (r : float8e24)
 {
 	r := 15;  // Error
 	r := 15.0;  // Error
-	r := fp(false, 1bv8, 0bv22); // Error
-	r := fp<8, 23>(1bv31); // Error
+	r := 0e1f22e8; // Error
+	r := 1e0f23e8; // Error
 	r := x; // Error
-	r := fp<8, 23>(1bv31) + fp<8, 23>(1bv31); // Error
-	r := fp<8, 24>(1bv32) + fp<8, 23>(1bv31); // Error
+	r := 1e0f23e8 + 1e0f23e8; // Error
+	r := 1e0f24e8 + 1e0f23e8; // Error
 	
 	return;
 }
\ No newline at end of file
diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl
index 9ed62579..2b901c94 100644
--- a/Test/floats/float1.bpl
+++ b/Test/floats/float1.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-procedure foo(x : float<8, 24>) returns (r : float<8, 24>)

-{

-	r := fp(false, 1bv8, 0bv23);

-	r := fp<8, 24>(1bv32);

-	r := x;

-	r := x + fp<8, 24>(1bv32);

-	r := fp<8, 24>(1bv32) + fp<8, 24>(1bv32);

-	assert(r == fp<8, 24>(2bv32));

-	

-	return;

+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo(x : float24e8) returns (r : float24e8)
+{
+	r := 0e1f24e8;
+	r := 1e0f24e8;
+	r := x;
+	r := x + 1e0f24e8;
+	r := 0e0f24e8 + 0e0f24e8;
+	assert(r == 0e1f24e8);
+	
+	return;
 }
\ No newline at end of file