diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index c04391772..b6c2deb3d 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -14,7 +14,7 @@
 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
@@ -117,61 +117,100 @@ public static BigFloat FromBigDec(BigDec v, int significandSize, int exponentSiz
     [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* 0+zero*e* 0-zero*e*
-       * Where * indicates an integer value (digit)
-       */
-      BIM sig, exp;
-      int sigSize, expSize;
-      bool isNeg;
-
-      if (s.IndexOf('f') == -1) {
-        String val;
-        int expIndex = s.IndexOf('e');
-        if (s[2] == 'z') //+zero, -zero
-        {
-          val = s.Substring(1, 5);
-          expIndex = s.IndexOf('e', expIndex + 1);
-        }
-        else //NaN, nan, +oo, -oo
-        {
-          val = s.Substring(1, 3);
+      * String must be either of the format [-]0x^.^e*f*e*
+      * or of the special value formats: 0NaN*e* 0nan*e* 0+oo*e* 0-oo*e*
+      * Where ^ indicates a hexadecimal value and * indicates an integer value
+      */
+
+      int posLastE = s.LastIndexOf('e');
+
+      int expSize = int.Parse(s.Substring(posLastE + 1));
+      if (expSize <= 1) {
+        throw new FormatException("Exponent size must be greater than 1");
+      }
+
+      int posLastF = s.LastIndexOf('f');
+      int posSig = posLastF + 1;
+      if (posLastF == -1) {//NaN, +oo, -oo
+        posSig = 4;
+      }
+
+      int sigSize = int.Parse(s.Substring(posSig, posLastE - posSig));
+      if (sigSize <= 1) {
+        throw new FormatException("Significand size must be greater than 1");
+      }
+
+      if (posLastF == -1) {//NaN, +oo, -oo
+        return new BigFloat(s.Substring(1, 3), sigSize, expSize);
+      }
+
+      bool isNeg = s[0] == '-';
+
+      int posX = s.IndexOf('x');
+      int posSecondLastE = s.LastIndexOf('e', posLastE - 1);
+
+      string hexSig = s.Substring(posX + 1, posSecondLastE - (posX + 1));
+      BIM oldExp = BIM.Parse(s.Substring(posSecondLastE + 1, posLastF - (posSecondLastE + 1)));
+
+      string binSig = string.Join(string.Empty,
+        hexSig.Select(
+          c => (c == '.' ? "." : Convert.ToString(Convert.ToInt32(c.ToString(), 16), 2).PadLeft(4, '0'))
+        )
+      );
+
+      int posDec = binSig.IndexOf('.');
+
+      binSig = binSig.Remove(posDec, 1);
+
+      int posFirstOne = binSig.IndexOf('1');
+      int posLastOne = binSig.LastIndexOf('1');
+
+      if (posFirstOne == -1) {
+        return new BigFloat(isNeg, 0, 0, sigSize, expSize);
+      }
+
+      binSig = binSig.Substring(posFirstOne, posLastOne - posFirstOne + 1);
+
+      BIM bias = two_n(expSize - 1) - 1;
+      BIM upperBound = 2 * bias + 1;
+
+      BIM newExp = 4 * oldExp + bias + (posDec - posFirstOne - 1);
+
+      if (newExp <= 0) {
+        if (-newExp <= (sigSize - 1) - binSig.Length) {
+          binSig = new string('0', (int)-newExp) + binSig;
+          newExp = 0;
         }
-        sigSize = int.Parse(s.Substring(val.Length + 1, expIndex - (val.Length + 1)));
-        expSize = int.Parse(s.Substring(expIndex + 1));
-        if (sigSize <= 0 || expSize <= 0)
-          throw new FormatException("Significand and Exponent sizes must be greater than 0");
-        return new BigFloat(val, sigSize, expSize);
+      } else {
+        binSig = binSig.Substring(1);
       }
 
-      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));
-      isNeg = s[0] == '-'; //We do this so that -0 is parsed correctly
-      
-      if (sigSize <= 0 || expSize <= 0)
-        throw new FormatException("Significand and Exponent sizes must be greater than 0");
+      if (newExp < 0 || newExp >= upperBound) {
+        throw new FormatException("The given exponent cannot fit in the bit size " + expSize);
+      }
 
-      sigSize = sigSize - 1; //Get rid of sign bit
-      sig = BIM.Abs(sig); //sig must be positive
-      //Uncomment if you want to shift the exponent for the user (i.e. 0e-1f24e8 --> 0e126f24e8)
-      //exp = exp + BIM.Pow(new BIM(2), expSize-1) - BIM.One;
+      binSig = binSig.PadRight(sigSize - 1, '0');
 
-      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 (binSig.Length > sigSize - 1) {
+        throw new FormatException("The given significand cannot fit in the bit size " + (sigSize - 1));
+      }
 
-      if (sig >= BIM.Pow(new BIM(2), sigSize))
-        throw new FormatException("The given significand " + sig + " cannot fit in the bit size " + (sigSize+1));
+      BIM newSig = 0;
+      foreach (char b in binSig) {
+        if (b != '.') {
+          newSig <<= 1;
+          newSig += b - '0';
+        }
+      }
 
-      return new BigFloat(isNeg, sig, exp, sigSize, expSize);
+      return new BigFloat(isNeg, newSig, newExp, 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.significandSize = significandSize;
       this.isNeg = isNeg;
       this.value = "";
     }
@@ -220,15 +259,51 @@ public override int GetHashCode() {
     [Pure]
     public override string/*!*/ ToString() {
       Contract.Ensures(Contract.Result<string>() != null);
-      String sigSize = significandSize.ToString();
-      String expSize = exponentSize.ToString();
-      if (value == "")
-      {
-        String sig = significand.ToString();
-        String exp = exponent.ToString();
-        return String.Format("{0}{1}e{2}f{3}e{4}", isNeg ? "-" : "", sig, exp, sigSize, expSize);
+      if (value == "") {
+        byte[] sigBytes = significand.ToByteArray();
+        StringBuilder binSig = new StringBuilder();
+
+        if (exponent == 0) {
+          binSig.Append('0');
+        } else {
+          binSig.Append('1'); //hidden bit
+        }
+
+        for (int i = significandSize - 2; i >= 0; --i) { //little endian
+         if (i / 8 < sigBytes.Length) {
+            binSig.Append((char) ('0' + ((sigBytes[i / 8] >> (i % 8)) & 1)));
+          } else {
+            binSig.Append('0');
+          }
+        }
+
+        BIM bias = two_n(exponentSize - 1) - 1;
+        if (exponent == 0) {
+          --bias;
+        }
+
+        int moveDec = ((int)((exponent - bias) % 4) + 4) % 4;
+        BIM finalExp = (exponent - bias - moveDec) / 4;
+
+        string leftBinSig = binSig.ToString().Substring(0, moveDec + 1);
+        string rightBinSig = binSig.ToString().Substring(moveDec + 1);
+
+        leftBinSig = new string('0', 4 - leftBinSig.Length % 4) + leftBinSig;
+        rightBinSig = rightBinSig + new string('0', 4 - rightBinSig.Length % 4);
+
+        StringBuilder leftHexSig = new StringBuilder();
+        StringBuilder rightHexSig = new StringBuilder();
+
+        for (int i = 0; i < leftBinSig.Length / 4; ++i) {
+          leftHexSig.AppendFormat("{0:X}", Convert.ToByte(leftBinSig.Substring(i * 4, 4), 2));
+        }
+        for (int i = 0; i < rightBinSig.Length / 4; ++i) {
+          rightHexSig.AppendFormat("{0:X}", Convert.ToByte(rightBinSig.Substring(i * 4, 4), 2));
+        }
+
+        return String.Format("{0}0x{1}.{2}e{3}f{4}e{5}", isNeg ? "-" : "", leftHexSig, rightHexSig, finalExp, significandSize, exponentSize);
       }
-      return String.Format("0{0}{1}e{2}", value, sigSize, expSize);
+      return String.Format("0{0}{1}e{2}", value, significandSize, exponentSize);
     }
 
 
@@ -461,7 +536,7 @@ public bool IsSpecialType {
       get {
         if (value == "")
           return false;
-        return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("+zero") || value.Equals("-zero"));
+        return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo"));
       }
     }
 
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index e3c8ce123..cc1baf532 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -118,6 +118,7 @@ private class BvBounds : Expr {
 CHARACTERS
   letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
   digit = "0123456789".
+  hexdigit = "0123456789ABCDEFabcdef".
   special = "'~#$^_.?`".
   glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
 
@@ -145,13 +146,11 @@ TOKENS
 
   decimal = 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} 
+	float = [ '-' ] '0' 'x' hexdigit {hexdigit} '.' hexdigit {hexdigit} 'e' [ '-' ] digit {digit} 'f' digit {digit} 'e' digit {digit} 
 										| '0' 'N' 'a' 'N' digit {digit} 'e' digit {digit}
 										| '0' 'n' 'a' 'n' digit {digit} 'e' digit {digit}
 										| '0' '+' 'o' 'o' digit {digit} 'e' digit {digit}
-										| '0' '-' 'o' 'o' digit {digit} 'e' digit {digit}
-										| '0' '+' 'z' 'e' 'r' 'o' digit {digit} 'e' digit {digit}
-										| '0' '-' 'z' 'e' 'r' 'o' digit {digit} 'e' digit {digit} .
+										| '0' '-' 'o' 'o' digit {digit} 'e' digit {digit} .
 
 COMMENTS FROM "/*" TO "*/" NESTED
 COMMENTS FROM "//" TO lf
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 82fafcd9d..221277891 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -2367,4 +2367,4 @@ public FatalError(string m): base(m) {}
 }
 
 
-}
\ No newline at end of file
+}
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index f72051385..84ca93e0d 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -267,42 +267,42 @@ static 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 = 49; i <= 57; ++i) start[i] = 57;
+		for (int i = 49; i <= 57; ++i) start[i] = 51;
 		for (int i = 34; i <= 34; ++i) start[i] = 6;
 		start[92] = 1; 
-		start[45] = 101; 
-		start[48] = 58; 
-		start[59] = 66; 
-		start[40] = 67; 
-		start[41] = 68; 
-		start[58] = 102; 
-		start[44] = 69; 
-		start[91] = 70; 
-		start[93] = 71; 
-		start[60] = 103; 
-		start[62] = 104; 
-		start[123] = 72; 
-		start[125] = 105; 
-		start[61] = 106; 
-		start[42] = 107; 
-		start[124] = 108; 
-		start[8660] = 75; 
-		start[8658] = 77; 
-		start[8656] = 78; 
-		start[38] = 79; 
-		start[8743] = 81; 
-		start[8744] = 83; 
-		start[33] = 109; 
-		start[8800] = 87; 
-		start[8804] = 88; 
-		start[8805] = 89; 
-		start[43] = 110; 
-		start[47] = 91; 
-		start[172] = 93; 
-		start[8704] = 96; 
-		start[8707] = 97; 
-		start[955] = 98; 
-		start[8226] = 100; 
+		start[48] = 52; 
+		start[45] = 96; 
+		start[59] = 61; 
+		start[40] = 62; 
+		start[41] = 63; 
+		start[58] = 97; 
+		start[44] = 64; 
+		start[91] = 65; 
+		start[93] = 66; 
+		start[60] = 98; 
+		start[62] = 99; 
+		start[123] = 67; 
+		start[125] = 100; 
+		start[61] = 101; 
+		start[42] = 102; 
+		start[124] = 103; 
+		start[8660] = 70; 
+		start[8658] = 72; 
+		start[8656] = 73; 
+		start[38] = 74; 
+		start[8743] = 76; 
+		start[8744] = 78; 
+		start[33] = 104; 
+		start[8800] = 82; 
+		start[8804] = 83; 
+		start[8805] = 84; 
+		start[43] = 105; 
+		start[47] = 86; 
+		start[172] = 88; 
+		start[8704] = 91; 
+		start[8707] = 92; 
+		start[955] = 93; 
+		start[8226] = 95; 
 		start[Buffer.EOF] = -1;
 
 	}
@@ -608,63 +608,63 @@ void CheckLiteral() {
 			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 59;}
+				else if (ch == 92) {AddCh(); goto case 53;}
 				else {goto case 0;}
 			case 7:
 				{t.kind = 4; break;}
 			case 8:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
+				else if (ch == '-') {AddCh(); goto case 9;}
 				else {goto case 0;}
 			case 9:
-				recEnd = pos; recKind = 6;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
-				else if (ch == 'e') {AddCh(); goto case 10;}
-				else {t.kind = 6; break;}
-			case 10:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
-				else if (ch == '-') {AddCh(); goto case 11;}
+				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;}
+				else {t.kind = 5; break;}
 			case 11:
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
 				else {goto case 0;}
 			case 12:
 				recEnd = pos; recKind = 6;
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+				else if (ch == 'e') {AddCh(); goto case 13;}
 				else {t.kind = 6; break;}
 			case 13:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;}
-				else if (ch == 'e') {AddCh(); goto case 14;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
+				else if (ch == '-') {AddCh(); goto case 14;}
 				else {goto case 0;}
 			case 14:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
-				else if (ch == '-') {AddCh(); goto case 15;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
 				else {goto case 0;}
 			case 15:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
-				else {goto case 0;}
+				recEnd = pos; recKind = 6;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
+				else {t.kind = 6; break;}
 			case 16:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
-				else if (ch == 'f') {AddCh(); goto case 17;}
+				if (ch == 'x') {AddCh(); goto case 17;}
 				else {goto case 0;}
 			case 17:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
+				if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 18;}
 				else {goto case 0;}
 			case 18:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
-				else if (ch == 'e') {AddCh(); goto case 19;}
+				if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 18;}
+				else if (ch == '.') {AddCh(); goto case 19;}
 				else {goto case 0;}
 			case 19:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;}
+				if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 20;}
 				else {goto case 0;}
 			case 20:
-				recEnd = pos; recKind = 7;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;}
-				else {t.kind = 7; break;}
+				if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'd' || ch == 'f') {AddCh(); goto case 20;}
+				else if (ch == 'e') {AddCh(); goto case 54;}
+				else {goto case 0;}
 			case 21:
-				if (ch == 'a') {AddCh(); goto case 22;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 22;}
 				else {goto case 0;}
 			case 22:
-				if (ch == 'N') {AddCh(); goto case 23;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 22;}
+				else if (ch == 'f') {AddCh(); goto case 23;}
 				else {goto case 0;}
 			case 23:
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;}
@@ -684,7 +684,7 @@ void CheckLiteral() {
 				if (ch == 'a') {AddCh(); goto case 28;}
 				else {goto case 0;}
 			case 28:
-				if (ch == 'n') {AddCh(); goto case 29;}
+				if (ch == 'N') {AddCh(); goto case 29;}
 				else {goto case 0;}
 			case 29:
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;}
@@ -701,259 +701,255 @@ void CheckLiteral() {
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;}
 				else {t.kind = 7; break;}
 			case 33:
-				if (ch == 'o') {AddCh(); goto case 34;}
+				if (ch == 'a') {AddCh(); goto case 34;}
 				else {goto case 0;}
 			case 34:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 35;}
+				if (ch == 'n') {AddCh(); goto case 35;}
 				else {goto case 0;}
 			case 35:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 35;}
-				else if (ch == 'e') {AddCh(); goto case 36;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;}
 				else {goto case 0;}
 			case 36:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 37;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;}
+				else if (ch == 'e') {AddCh(); goto case 37;}
 				else {goto case 0;}
 			case 37:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;}
+				else {goto case 0;}
+			case 38:
 				recEnd = pos; recKind = 7;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 37;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;}
 				else {t.kind = 7; break;}
-			case 38:
-				if (ch == 'o') {AddCh(); goto case 39;}
-				else {goto case 0;}
 			case 39:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 40;}
+				if (ch == 'o') {AddCh(); goto case 40;}
 				else {goto case 0;}
 			case 40:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 40;}
-				else if (ch == 'e') {AddCh(); goto case 41;}
+				if (ch == 'o') {AddCh(); goto case 41;}
 				else {goto case 0;}
 			case 41:
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;}
 				else {goto case 0;}
 			case 42:
-				recEnd = pos; recKind = 7;
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;}
-				else {t.kind = 7; break;}
+				else if (ch == 'e') {AddCh(); goto case 43;}
+				else {goto case 0;}
 			case 43:
-				if (ch == 'e') {AddCh(); goto case 44;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;}
 				else {goto case 0;}
 			case 44:
-				if (ch == 'r') {AddCh(); goto case 45;}
-				else {goto case 0;}
+				recEnd = pos; recKind = 7;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;}
+				else {t.kind = 7; break;}
 			case 45:
 				if (ch == 'o') {AddCh(); goto case 46;}
 				else {goto case 0;}
 			case 46:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 47;}
+				if (ch == 'o') {AddCh(); goto case 47;}
 				else {goto case 0;}
 			case 47:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 47;}
-				else if (ch == 'e') {AddCh(); goto case 48;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 48;}
 				else {goto case 0;}
 			case 48:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 49;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 48;}
+				else if (ch == 'e') {AddCh(); goto case 49;}
 				else {goto case 0;}
 			case 49:
-				recEnd = pos; recKind = 7;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 49;}
-				else {t.kind = 7; break;}
-			case 50:
-				if (ch == 'e') {AddCh(); goto case 51;}
-				else {goto case 0;}
-			case 51:
-				if (ch == 'r') {AddCh(); goto case 52;}
-				else {goto case 0;}
-			case 52:
-				if (ch == 'o') {AddCh(); goto case 53;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;}
 				else {goto case 0;}
-			case 53:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 54;}
-				else {goto case 0;}
-			case 54:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 54;}
-				else if (ch == 'e') {AddCh(); goto case 55;}
-				else {goto case 0;}
-			case 55:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 56;}
-				else {goto case 0;}
-			case 56:
+			case 50:
 				recEnd = pos; recKind = 7;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 56;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;}
 				else {t.kind = 7; break;}
-			case 57:
+			case 51:
 				recEnd = pos; recKind = 3;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 57;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 51;}
 				else if (ch == 'b') {AddCh(); goto case 3;}
-				else if (ch == 'e') {AddCh(); goto case 60;}
-				else if (ch == '.') {AddCh(); goto case 8;}
+				else if (ch == 'e') {AddCh(); goto case 8;}
+				else if (ch == '.') {AddCh(); goto case 11;}
 				else {t.kind = 3; break;}
-			case 58:
+			case 52:
 				recEnd = pos; recKind = 3;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 57;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 51;}
 				else if (ch == 'b') {AddCh(); goto case 3;}
-				else if (ch == 'e') {AddCh(); goto case 60;}
-				else if (ch == '.') {AddCh(); goto case 8;}
-				else if (ch == 'N') {AddCh(); goto case 21;}
-				else if (ch == 'n') {AddCh(); goto case 27;}
-				else if (ch == '+') {AddCh(); goto case 61;}
-				else if (ch == '-') {AddCh(); goto case 62;}
+				else if (ch == 'e') {AddCh(); goto case 8;}
+				else if (ch == '.') {AddCh(); goto case 11;}
+				else if (ch == 'x') {AddCh(); goto case 17;}
+				else if (ch == 'N') {AddCh(); goto case 27;}
+				else if (ch == 'n') {AddCh(); goto case 33;}
+				else if (ch == '+') {AddCh(); goto case 39;}
+				else if (ch == '-') {AddCh(); goto case 45;}
 				else {t.kind = 3; break;}
-			case 59:
-				if (ch == '"') {AddCh(); goto case 63;}
+			case 53:
+				if (ch == '"') {AddCh(); goto case 55;}
 				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 59;}
-				else {goto case 0;}
-			case 60:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 64;}
-				else if (ch == '-') {AddCh(); goto case 65;}
-				else {goto case 0;}
-			case 61:
-				if (ch == 'o') {AddCh(); goto case 33;}
-				else if (ch == 'z') {AddCh(); goto case 43;}
+				else if (ch == 92) {AddCh(); goto case 53;}
 				else {goto case 0;}
-			case 62:
-				if (ch == 'o') {AddCh(); goto case 38;}
-				else if (ch == 'z') {AddCh(); goto case 50;}
+			case 54:
+				if (ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'd' || ch == 'f') {AddCh(); goto case 20;}
+				else if (ch >= '0' && ch <= '9') {AddCh(); goto case 56;}
+				else if (ch == 'e') {AddCh(); goto case 54;}
+				else if (ch == '-') {AddCh(); goto case 21;}
 				else {goto case 0;}
-			case 63:
+			case 55:
 				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 59;}
+				else if (ch == 92) {AddCh(); goto case 53;}
 				else {t.kind = 4; break;}
-			case 64:
-				recEnd = pos; recKind = 5;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 64;}
-				else if (ch == 'f') {AddCh(); goto case 17;}
-				else {t.kind = 5; break;}
-			case 65:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 64;}
+			case 56:
+				if (ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'd') {AddCh(); goto case 20;}
+				else if (ch >= '0' && ch <= '9') {AddCh(); goto case 56;}
+				else if (ch == 'e') {AddCh(); goto case 54;}
+				else if (ch == 'f') {AddCh(); goto case 57;}
 				else {goto case 0;}
-			case 66:
+			case 57:
+				if (ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'd' || ch == 'f') {AddCh(); goto case 20;}
+				else if (ch >= '0' && ch <= '9') {AddCh(); goto case 58;}
+				else if (ch == 'e') {AddCh(); goto case 54;}
+				else {goto case 0;}
+			case 58:
+				if (ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'd' || ch == 'f') {AddCh(); goto case 20;}
+				else if (ch >= '0' && ch <= '9') {AddCh(); goto case 58;}
+				else if (ch == 'e') {AddCh(); goto case 59;}
+				else {goto case 0;}
+			case 59:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 60;}
+				else if (ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'd' || ch == 'f') {AddCh(); goto case 20;}
+				else if (ch == 'e') {AddCh(); goto case 54;}
+				else if (ch == '-') {AddCh(); goto case 21;}
+				else {goto case 0;}
+			case 60:
+				recEnd = pos; recKind = 7;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 60;}
+				else if (ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'd') {AddCh(); goto case 20;}
+				else if (ch == 'e') {AddCh(); goto case 54;}
+				else if (ch == 'f') {AddCh(); goto case 57;}
+				else {t.kind = 7; break;}
+			case 61:
 				{t.kind = 9; break;}
-			case 67:
+			case 62:
 				{t.kind = 10; break;}
-			case 68:
+			case 63:
 				{t.kind = 11; break;}
-			case 69:
+			case 64:
 				{t.kind = 13; break;}
-			case 70:
+			case 65:
 				{t.kind = 18; break;}
-			case 71:
+			case 66:
 				{t.kind = 19; break;}
-			case 72:
+			case 67:
 				{t.kind = 28; break;}
-			case 73:
+			case 68:
 				{t.kind = 51; break;}
-			case 74:
+			case 69:
 				{t.kind = 56; break;}
-			case 75:
+			case 70:
 				{t.kind = 57; break;}
-			case 76:
+			case 71:
 				{t.kind = 58; break;}
-			case 77:
+			case 72:
 				{t.kind = 59; break;}
-			case 78:
+			case 73:
 				{t.kind = 61; break;}
-			case 79:
-				if (ch == '&') {AddCh(); goto case 80;}
+			case 74:
+				if (ch == '&') {AddCh(); goto case 75;}
 				else {goto case 0;}
-			case 80:
+			case 75:
 				{t.kind = 62; break;}
-			case 81:
+			case 76:
 				{t.kind = 63; break;}
-			case 82:
+			case 77:
 				{t.kind = 64; break;}
-			case 83:
+			case 78:
 				{t.kind = 65; break;}
-			case 84:
+			case 79:
 				{t.kind = 68; break;}
-			case 85:
+			case 80:
 				{t.kind = 69; break;}
-			case 86:
+			case 81:
 				{t.kind = 70; break;}
-			case 87:
+			case 82:
 				{t.kind = 71; break;}
-			case 88:
+			case 83:
 				{t.kind = 72; break;}
-			case 89:
+			case 84:
 				{t.kind = 73; break;}
-			case 90:
+			case 85:
 				{t.kind = 74; break;}
-			case 91:
+			case 86:
 				{t.kind = 79; break;}
-			case 92:
+			case 87:
 				{t.kind = 80; break;}
-			case 93:
+			case 88:
 				{t.kind = 82; break;}
-			case 94:
+			case 89:
 				{t.kind = 96; break;}
-			case 95:
+			case 90:
 				{t.kind = 97; break;}
-			case 96:
+			case 91:
 				{t.kind = 100; break;}
-			case 97:
+			case 92:
 				{t.kind = 102; break;}
-			case 98:
+			case 93:
 				{t.kind = 104; break;}
-			case 99:
+			case 94:
 				{t.kind = 105; break;}
-			case 100:
+			case 95:
 				{t.kind = 106; break;}
-			case 101:
+			case 96:
 				recEnd = pos; recKind = 76;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;}
+				if (ch == '0') {AddCh(); goto case 16;}
 				else {t.kind = 76; break;}
-			case 102:
+			case 97:
 				recEnd = pos; recKind = 12;
-				if (ch == '=') {AddCh(); goto case 73;}
-				else if (ch == ':') {AddCh(); goto case 99;}
+				if (ch == '=') {AddCh(); goto case 68;}
+				else if (ch == ':') {AddCh(); goto case 94;}
 				else {t.kind = 12; break;}
-			case 103:
+			case 98:
 				recEnd = pos; recKind = 20;
-				if (ch == '=') {AddCh(); goto case 111;}
-				else if (ch == ':') {AddCh(); goto case 86;}
+				if (ch == '=') {AddCh(); goto case 106;}
+				else if (ch == ':') {AddCh(); goto case 81;}
 				else {t.kind = 20; break;}
-			case 104:
+			case 99:
 				recEnd = pos; recKind = 21;
-				if (ch == '=') {AddCh(); goto case 84;}
+				if (ch == '=') {AddCh(); goto case 79;}
 				else {t.kind = 21; break;}
-			case 105:
+			case 100:
 				recEnd = pos; recKind = 29;
-				if (ch == '|') {AddCh(); goto case 95;}
+				if (ch == '|') {AddCh(); goto case 90;}
 				else {t.kind = 29; break;}
-			case 106:
+			case 101:
 				recEnd = pos; recKind = 32;
-				if (ch == '=') {AddCh(); goto case 112;}
+				if (ch == '=') {AddCh(); goto case 107;}
 				else {t.kind = 32; break;}
-			case 107:
+			case 102:
 				recEnd = pos; recKind = 45;
-				if (ch == '*') {AddCh(); goto case 92;}
+				if (ch == '*') {AddCh(); goto case 87;}
 				else {t.kind = 45; break;}
-			case 108:
+			case 103:
 				recEnd = pos; recKind = 55;
-				if (ch == '|') {AddCh(); goto case 82;}
-				else if (ch == '{') {AddCh(); goto case 94;}
+				if (ch == '|') {AddCh(); goto case 77;}
+				else if (ch == '{') {AddCh(); goto case 89;}
 				else {t.kind = 55; break;}
-			case 109:
+			case 104:
 				recEnd = pos; recKind = 81;
-				if (ch == '=') {AddCh(); goto case 85;}
+				if (ch == '=') {AddCh(); goto case 80;}
 				else {t.kind = 81; break;}
-			case 110:
+			case 105:
 				recEnd = pos; recKind = 75;
-				if (ch == '+') {AddCh(); goto case 90;}
+				if (ch == '+') {AddCh(); goto case 85;}
 				else {t.kind = 75; break;}
-			case 111:
+			case 106:
 				recEnd = pos; recKind = 67;
-				if (ch == '=') {AddCh(); goto case 113;}
+				if (ch == '=') {AddCh(); goto case 108;}
 				else {t.kind = 67; break;}
-			case 112:
+			case 107:
 				recEnd = pos; recKind = 66;
-				if (ch == '>') {AddCh(); goto case 76;}
+				if (ch == '>') {AddCh(); goto case 71;}
 				else {t.kind = 66; break;}
-			case 113:
+			case 108:
 				recEnd = pos; recKind = 60;
-				if (ch == '>') {AddCh(); goto case 74;}
+				if (ch == '>') {AddCh(); goto case 69;}
 				else {t.kind = 60; break;}
 
 		}
@@ -1000,4 +996,4 @@ private void SetScannerBehindT() {
 public delegate void ErrorProc(int n, string filename, int line, int col);
 
 
-}
\ No newline at end of file
+}
diff --git a/Test/floats/BasicOperators1.bpl b/Test/floats/BasicOperators1.bpl
index 80ec77828..12c159e12 100644
--- a/Test/floats/BasicOperators1.bpl
+++ b/Test/floats/BasicOperators1.bpl
@@ -8,20 +8,20 @@ procedure main() returns () {
   z := x + y;
   z := x - y;
   z := x * y;
-  assume(!FEQ(y,0e0f24e8));
+  assume(!FEQ(y, 0x0.0e0f24e8));
   z := x / y;
   
-  z := (0e127f24e8 + 0e127f24e8 + 0e0f24e8);
-  assert(z == 0e128f24e8);
+  z := (0x1.0e0f24e8 + 0x1.0e0f24e8 + 0x0.0e0f24e8);
+  assert(z == 0x2.0e0f24e8);
   
-  z := 0e128f24e8 - 0e127f24e8;
-  assert(z == 0e127f24e8);
+  z := 0x2.0e0f24e8 - 0x1.0e0f24e8;
+  assert(z == 0x1.0e0f24e8);
   
-  z := 0e127f24e8 * 0e127f24e8;
-  assert(z == 0e127f24e8);
+  z := 0x1.0e0f24e8 * 0x1.0e0f24e8;
+  assert(z == 0x1.0e0f24e8);
   
-  z := 0e127f24e8 / 0e127f24e8;
-  assert(z == 0e127f24e8);
+  z := 0x1.0e0f24e8 / 0x1.0e0f24e8;
+  assert(z == 0x1.0e0f24e8);
   
   return;
 }
diff --git a/Test/floats/BasicOperators2.bpl b/Test/floats/BasicOperators2.bpl
index 0bb66bcd6..17c637e5a 100644
--- a/Test/floats/BasicOperators2.bpl
+++ b/Test/floats/BasicOperators2.bpl
@@ -5,10 +5,10 @@ procedure main() returns () {
   var y : float53e11;
   var z : float53e11;
   var r : float53e11;
-  x := 0e1063f53e11;
-  y := x + 0e1023f53e11;
-  z := x - 0e1023f53e11;
+  x := 0x1.0e10f53e11;
+  y := x + 0x1.0e0f53e11;
+  z := x - 0x1.0e0f53e11;
   r := y - z;
   
-  assert r == 0e1024f53e11;
+  assert r == 0x2.0e0f53e11;
 }
diff --git a/Test/floats/BasicOperators3.bpl b/Test/floats/BasicOperators3.bpl
index 1109505e0..e476cff35 100644
--- a/Test/floats/BasicOperators3.bpl
+++ b/Test/floats/BasicOperators3.bpl
@@ -5,9 +5,9 @@ procedure main() returns () {
   var y : float24e8;
   var z : float24e8;
   var r : float24e8;
-  x := 0e167f24e8;
-  y := x + 0e127f24e8;
-  z := x - 0e127f24e8;
+  x := 0x1.0e10f24e8;
+  y := x + 0x1.0e0f24e8;
+  z := x - 0x1.0e0f24e8;
   r := y - z;
-  assert r == 0e128f24e8;
+  assert r == 0x2.0e0f24e8;
 }
diff --git a/Test/floats/BasicOperators4.bpl b/Test/floats/BasicOperators4.bpl
index 669c0c91e..45cedd4bb 100644
--- a/Test/floats/BasicOperators4.bpl
+++ b/Test/floats/BasicOperators4.bpl
@@ -6,13 +6,13 @@ type f = float;
 
 procedure foo(x : float) returns (r : f)
 {
-  r := 0e128f24e8;
-  r := 1e127f24e8;
+  r := 0x2.0e0f24e8;
+  r := 0x1.000002e0f24e8;
   r := x;
-  r := x * 1e127f24e8;
-  r := x + 1e127f24e8;
-  r := 0e127f24e8 + 0e127f24e8;
-  assert(r == 0e128f24e8);
+  r := x * 0x1.000002e0f24e8;
+  r := x + 0x1.000002e0f24e8;
+  r := 0x1.0e0f24e8 + 0x1.0e0f24e8;
+  assert(r == 0x2.0e0f24e8);
   
   return;
 }
diff --git a/Test/floats/ConstSyntax1.bpl b/Test/floats/ConstSyntax1.bpl
index f5147ea57..ff1945aef 100644
--- a/Test/floats/ConstSyntax1.bpl
+++ b/Test/floats/ConstSyntax1.bpl
@@ -4,11 +4,11 @@ procedure foo(x : real) returns (r : float8e24)
 {
   r := 15;  // Error
   r := 15.0;  // Error
-  r := 0e1f22e8; // Error
-  r := 1e0f23e8; // Error
+  r := 0x4.0e-32f22e8; // Error
+  r := 0x0.00001e-32f23e8; // Error
   r := x; // Error
-  r := 1e0f23e8 + 1e0f23e8; // Error
-  r := 1e0f24e8 + 1e0f23e8; // Error
+  r := 0x0.00001e-32f23e8 + 0x0.00001e-32f23e8; // Error
+  r := 0x0.000008e-32f24e8 + 0x0.00001e-32f23e8; // Error
   
   return;
 }
diff --git a/Test/floats/ConstSyntax1.bpl.expect b/Test/floats/ConstSyntax1.bpl.expect
index 8ba283242..2e0b61647 100644
--- a/Test/floats/ConstSyntax1.bpl.expect
+++ b/Test/floats/ConstSyntax1.bpl.expect
@@ -4,5 +4,5 @@ ConstSyntax1.bpl(7,2): Error: mismatched types in assignment command (cannot ass
 ConstSyntax1.bpl(8,2): Error: mismatched types in assignment command (cannot assign float23e8 to float8e24)
 ConstSyntax1.bpl(9,2): Error: mismatched types in assignment command (cannot assign real to float8e24)
 ConstSyntax1.bpl(10,2): Error: mismatched types in assignment command (cannot assign float23e8 to float8e24)
-ConstSyntax1.bpl(11,16): Error: invalid argument types (float24e8 and float23e8) to binary operator +
+ConstSyntax1.bpl(11,27): Error: invalid argument types (float24e8 and float23e8) to binary operator +
 7 type checking errors detected in ConstSyntax1.bpl
diff --git a/Test/floats/ConstSyntax2.bpl b/Test/floats/ConstSyntax2.bpl
index 6382d0874..54326835b 100644
--- a/Test/floats/ConstSyntax2.bpl
+++ b/Test/floats/ConstSyntax2.bpl
@@ -2,12 +2,12 @@
 // RUN: %diff "%s.expect" "%t"
 procedure foo(x : float24e8) returns (r : float24e8)
 {
-  r := 0e128f24e8;
-  r := 1e127f24e8;
+  r := 0x2.0e0f24e8;
+  r := 0x1.000002e0f24e8;
   r := x;
-  r := x + 1e127f24e8;
-  r := 0e127f24e8 + 0e127f24e8;
-  assert(r == 0e128f24e8);
+  r := x + 0x1.000002e0f24e8;
+  r := 0x1.0e0f24e8 + 0x1.0e0f24e8;
+  assert(r == 0x2.0e0f24e8);
   
   return;
 }
diff --git a/Test/floats/ConstSyntax3.bpl b/Test/floats/ConstSyntax3.bpl
index 5c5648e94..d43550652 100644
--- a/Test/floats/ConstSyntax3.bpl
+++ b/Test/floats/ConstSyntax3.bpl
@@ -1,22 +1,33 @@
 // RUN: %boogie -proverWarnings:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 procedure main() returns () {
+
+  var a : float2e1;
+  var b : float1e2;
+  var c : float2e2;
+
   var f : float24e8;
   var d : float53e11;
+
+  a := 0x0.0e0f2e1; //Error
+  b := 0x0.0e0f1e2; //Error
+  c := 0x0.0e0f2e2; //No Error
   
-  f := 0e-1f24e8; //Error
-  f := 0e256f24e8; //Error
-  f := 0e255f24e8; //No Error
+  f := 0x0.000004e-32f24e8; //Error
+  f := 0x0.000008e-32f24e8; //No Error
+  f := 0x1.0e32f24e8; //Error
+  f := 0x0.8e32f24e8; //No Error
   
-  f := 8388608e0f24e8; //Error
-  f := -8388608e0f24e8; //Error
-  f := 8388607e0f24e8; //No Error
+  f := 0x1.ffffffe0f24e8; //Error
+  f := -0x1.ffffffe0f24e8; //Error
+  f := 0x0.ffffffe0f24e8; //No Error
   
-  d := 0e-1f53e11; //Error
-  d := 0e2048f53e11; //Error
-  d := 0e2047f53e11; //No Error
+  d := 0x0.0000000000002e-256f53e11; //Error
+  d := 0x0.0000000000004e-256f53e11; //No Error
+  d := 0x1.0e256f53e11; //Error
+  d := 0x0.8e256f53e11; //No Error
   
-  d := 4503599627370496e0f53e11; //Error
-  d := -4503599627370496e0f53e11; //Error
-  d := 4503599627370495e0f53e11; //No Error
+  d := 0x3.fffffffffffffe0f53e11; //Error
+  d := -0x3.fffffffffffffe0f53e11; //Error
+  d := 0x1.fffffffffffffe0f53e11; //No Error
 }
diff --git a/Test/floats/ConstSyntax3.bpl.expect b/Test/floats/ConstSyntax3.bpl.expect
index 6fb149b9f..644ae3c18 100644
--- a/Test/floats/ConstSyntax3.bpl.expect
+++ b/Test/floats/ConstSyntax3.bpl.expect
@@ -1,9 +1,11 @@
-ConstSyntax3.bpl(7,8): error: incorrectly formatted floating point, The given exponent -1 cannot fit in the bit size 8
-ConstSyntax3.bpl(8,8): error: incorrectly formatted floating point, The given exponent 256 cannot fit in the bit size 8
-ConstSyntax3.bpl(11,8): error: incorrectly formatted floating point, The given significand 8388608 cannot fit in the bit size 24
-ConstSyntax3.bpl(12,8): error: incorrectly formatted floating point, The given significand 8388608 cannot fit in the bit size 24
-ConstSyntax3.bpl(15,8): error: incorrectly formatted floating point, The given exponent -1 cannot fit in the bit size 11
-ConstSyntax3.bpl(16,8): error: incorrectly formatted floating point, The given exponent 2048 cannot fit in the bit size 11
-ConstSyntax3.bpl(19,8): error: incorrectly formatted floating point, The given significand 4503599627370496 cannot fit in the bit size 53
-ConstSyntax3.bpl(20,8): error: incorrectly formatted floating point, The given significand 4503599627370496 cannot fit in the bit size 53
-8 parse errors detected in ConstSyntax3.bpl
+ConstSyntax3.bpl(12,8): error: incorrectly formatted floating point, Exponent size must be greater than 1
+ConstSyntax3.bpl(13,8): error: incorrectly formatted floating point, Significand size must be greater than 1
+ConstSyntax3.bpl(16,8): error: incorrectly formatted floating point, The given exponent cannot fit in the bit size 8
+ConstSyntax3.bpl(18,8): error: incorrectly formatted floating point, The given exponent cannot fit in the bit size 8
+ConstSyntax3.bpl(21,8): error: incorrectly formatted floating point, The given significand cannot fit in the bit size 23
+ConstSyntax3.bpl(22,8): error: incorrectly formatted floating point, The given significand cannot fit in the bit size 23
+ConstSyntax3.bpl(25,8): error: incorrectly formatted floating point, The given exponent cannot fit in the bit size 11
+ConstSyntax3.bpl(27,8): error: incorrectly formatted floating point, The given exponent cannot fit in the bit size 11
+ConstSyntax3.bpl(30,8): error: incorrectly formatted floating point, The given significand cannot fit in the bit size 52
+ConstSyntax3.bpl(31,8): error: incorrectly formatted floating point, The given significand cannot fit in the bit size 52
+10 parse errors detected in ConstSyntax3.bpl
diff --git a/Test/floats/CorrectTypeConv.bpl b/Test/floats/CorrectTypeConv.bpl
index d2bdafa11..5ae152d1b 100644
--- a/Test/floats/CorrectTypeConv.bpl
+++ b/Test/floats/CorrectTypeConv.bpl
@@ -20,8 +20,8 @@ procedure main() returns () {
   f32 := TO_FLOAT32_BV32(0bv32);
   f64 := TO_FLOAT64_BV64(0bv64);
   
-  f32 := TO_FLOAT32_FLOAT64(0e0f53e11);
-  f64 := TO_FLOAT64_FLOAT32(0e0f24e8);
+  f32 := TO_FLOAT32_FLOAT64(0x0.0e0f53e11);
+  f64 := TO_FLOAT64_FLOAT32(0x0.0e0f24e8);
   
   f32 := TO_FLOAT32_FLOAT64(f64);
   f64 := TO_FLOAT64_FLOAT32(f32);
diff --git a/Test/floats/Equal2.bpl b/Test/floats/Equal2.bpl
index 04715df97..f23c6bb9a 100644
--- a/Test/floats/Equal2.bpl
+++ b/Test/floats/Equal2.bpl
@@ -7,8 +7,8 @@ function {:builtin "fp.eq"} FEQ(float,float) returns (bool);
 
 procedure Main()
 {
-  assert 0e0f24e8 != -0e0f24e8;
-  assert FEQ(0e0f24e8,-0e0f24e8);
+  assert 0x0.0e0f24e8 != -0x0.0e0f24e8;
+  assert FEQ(0x0.0e0f24e8,-0x0.0e0f24e8);
   assert 0+oo24e8 != 0-oo24e8;
   assert !FEQ(0+oo24e8,0-oo24e8);
 }
diff --git a/Test/floats/EvaluateSignBit.bpl b/Test/floats/EvaluateSignBit.bpl
index 61275f1cc..84ebfa6ce 100644
--- a/Test/floats/EvaluateSignBit.bpl
+++ b/Test/floats/EvaluateSignBit.bpl
@@ -5,11 +5,11 @@ procedure foo()
   var a : float53e11;
   var b : float53e11;
   var c : float53e11;
-  a := 2533274790395904e1028f53e11; //50.0
-  b := 3483252836794368e1023f53e11; //1.99
-  c := -3483252836794368e1023f53e11; //-1.99
+  a := 0x3.2e1f53e11; //50.0
+  b := 0x1.fd70a3d70a3d7e0f53e11; //1.99
+  c := -0x1.fd70a3d70a3d7e0f53e11; //-1.99
   b := (b * a) / a;
   c := (c * a) / a;
-  assert (b > 0e0f53e11); //b should be positive
-  assert (c < 0e0f53e11); //c should be negative
+  assert (b > 0x0.0e0f53e11); //b should be positive
+  assert (c < 0x0.0e0f53e11); //c should be negative
 }
diff --git a/Test/floats/IncorrectTypeConv.bpl b/Test/floats/IncorrectTypeConv.bpl
index 878e7f1d5..6b89e109d 100644
--- a/Test/floats/IncorrectTypeConv.bpl
+++ b/Test/floats/IncorrectTypeConv.bpl
@@ -13,8 +13,8 @@ procedure foo(x : float24e8) returns (r : float24e8) {
   r := TO_FLOAT823_REAL(5.0); // Error
   r := TO_FLOAT823_BV31(0bv31); // Error
   r := TO_FLOAT823_BV32(0bv32); // Error
-  r := TO_FLOAT823_FLOAT824(0e0f24e8); // Error
-  r := TO_FLOAT824_FLOAT823(0e0f23e8); // Error
+  r := TO_FLOAT823_FLOAT824(0x0.0e0f24e8); // Error
+  r := TO_FLOAT824_FLOAT823(0x0.0e0f23e8); // Error
   
   r := TO_FLOAT823_FLOAT824(x); // Error
   r := TO_FLOAT824_FLOAT823(x); // Error
diff --git a/Test/floats/RemovedZeroSpecialValue.bpl b/Test/floats/RemovedZeroSpecialValue.bpl
new file mode 100644
index 000000000..0531d309a
--- /dev/null
+++ b/Test/floats/RemovedZeroSpecialValue.bpl
@@ -0,0 +1,8 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo() returns (r : float24e8) {
+  var d : float53e11;
+
+  d := 0+zero53e11;
+  d := 0-zero53e11;
+}
diff --git a/Test/floats/RemovedZeroSpecialValue.bpl.expect b/Test/floats/RemovedZeroSpecialValue.bpl.expect
new file mode 100644
index 000000000..0d1ea5a4a
--- /dev/null
+++ b/Test/floats/RemovedZeroSpecialValue.bpl.expect
@@ -0,0 +1,3 @@
+RemovedZeroSpecialValue.bpl(6,9): Error: undeclared identifier: zero53e11
+RemovedZeroSpecialValue.bpl(7,9): Error: undeclared identifier: zero53e11
+2 name resolution errors detected in RemovedZeroSpecialValue.bpl
diff --git a/Test/floats/RoundingMode1.bpl b/Test/floats/RoundingMode1.bpl
index b6ea469c7..8f7eab751 100644
--- a/Test/floats/RoundingMode1.bpl
+++ b/Test/floats/RoundingMode1.bpl
@@ -12,20 +12,20 @@ procedure {:inline 1} roundingTest(f1: float32, f2: float32)
 
   rm := RNE;
   rneSum := f1 + f2;
-  assert EQ(rneSum,1e127f24e8);
+  assert EQ(rneSum,0x1.000002e0f24e8);
 
   rm := RTN;
   rtnSum := ADD(rm,f1,f2);
-  assert EQ(rtnSum,0e127f24e8);
+  assert EQ(rtnSum,0x1.0e0f24e8);
 }
 
 procedure Main()
 {
   var f1,f2: float32;
 
-  call roundingTest(0e127f24e8, 4194304e103f24e8);
+  call roundingTest(0x1.0e0f24e8, 0x1.8e-6f24e8);
 
-  assume 8388607e126f24e8 < f1 && f1 < 1e127f24e8;
-  assume 4194303e103f24e8 < f2 && f2 < 4194305e103f24e8;
+  assume 0x0.ffffffe0f24e8 < f1 && f1 < 0x1.000002e0f24e8;
+  assume 0x1.7ffffee-6f24e8 < f2 && f2 < 0x1.800002e-6f24e8;
   call roundingTest(f1, f2);
 }
diff --git a/Test/floats/SpecialValues.bpl b/Test/floats/SpecialValues.bpl
index a9df9a873..4a86dfbe3 100644
--- a/Test/floats/SpecialValues.bpl
+++ b/Test/floats/SpecialValues.bpl
@@ -7,25 +7,29 @@ procedure foo() returns (r : float24e8) {
   r := 0nan24e8;
   assert !FEQ(r,0NaN24e8);  //NaN != NaN
   r := 0+oo24e8;
-  assert r == 0e255f24e8;
   r := 0-oo24e8;
-  assert r == -0e255f24e8;
-  r := -5e255f24e8;
+  r := 0x1.0e32f24e8; //Error: this is a synonym for +oo, which is disallowed
+  r := -0x1.0e32f24e8; //Error: this is a synonym for -oo, which is disallowed
+  r := -0x5.0e32f24e8; //Error: NaN values are disallowed
 
   d := 0NaN53e11;
   d := 0nan53e11;
   assert !DEQ(d,0NaN53e11);
   d := 0+oo53e11;
-  assert DEQ(d,0e2047f53e11);
   d := 0-oo53e11;
-  assert DEQ(d,-0e2047f53e11);
-  d := -200e2000f53e11;
+  d := 0;
+  d := 0x1.0e256f53e11;
+  d := -0x1.0e256f53e11;
+  d := -0x5.0e256f53e11;
 
-  d := 0+zero53e11;
-  assert d == 0e0f53e11;
+  d := 0+zero53e11; //Error: there are no longer special values for +zero and -zero
   d := 0-zero53e11;
-  assert d == -0e0f53e11;
-  assert DEQ(0+zero53e11, 0-zero53e11);
+
+  d := 0x0.0e0f53e11;
+  assert d == 0x0.0e0f53e11;
+  d := -0x0.0e0f53e11;
+  assert d == -0x0.0e0f53e11;
+  assert(DEQ(0x0.0e0f53e11, -0x0.0e0f53e11));
 
   return;
 }
diff --git a/Test/floats/SpecialValues.bpl.expect b/Test/floats/SpecialValues.bpl.expect
index 37fad75c9..a96641a5c 100644
--- a/Test/floats/SpecialValues.bpl.expect
+++ b/Test/floats/SpecialValues.bpl.expect
@@ -1,2 +1,7 @@
-
-Boogie program verifier finished with 1 verified, 0 errors
+SpecialValues.bpl(11,8): error: incorrectly formatted floating point, The given exponent cannot fit in the bit size 8
+SpecialValues.bpl(12,8): error: incorrectly formatted floating point, The given exponent cannot fit in the bit size 8
+SpecialValues.bpl(13,8): error: incorrectly formatted floating point, The given exponent cannot fit in the bit size 8
+SpecialValues.bpl(21,8): error: incorrectly formatted floating point, The given exponent cannot fit in the bit size 11
+SpecialValues.bpl(22,8): error: incorrectly formatted floating point, The given exponent cannot fit in the bit size 11
+SpecialValues.bpl(23,8): error: incorrectly formatted floating point, The given exponent cannot fit in the bit size 11
+6 parse errors detected in SpecialValues.bpl
diff --git a/Test/floats/TypeConvConst.bpl b/Test/floats/TypeConvConst.bpl
index 1b5328bf8..bd2024c14 100644
--- a/Test/floats/TypeConvConst.bpl
+++ b/Test/floats/TypeConvConst.bpl
@@ -12,23 +12,23 @@ procedure main() returns () {
   var d : float53e11;
   var dc : float53e11;
   
-  f := 2097152e129f24e8;
+  f := 0x5.0e0f24e8;
   fc := TO_FLOAT32_INT(5);
   assert(f == fc);
   
-  f := -0e126f24e8;
+  f := -0x0.8e0f24e8;
   fc := TO_FLOAT32_REAL(-0.5);
   assert(f == fc);
   
-  f := 1048576e128f24e8;
+  f := 0x2.4e0f24e8;
   fc := TO_FLOAT32_REAL(2.25);
   assert(f == fc);
   
-  d := 1125899906842624e1025f53e11;
+  d := 0x5.0e0f53e11;
   dc := TO_FLOAT64_INT(5);
   assert(d == dc);
   
-  d := 562949953421312e1024f53e11;
+  d := 0x2.4e0f53e11;
   dc := TO_FLOAT64_REAL(2.25);
   assert(d == dc);
 }
diff --git a/Test/floats/TypeMismatch2.bpl b/Test/floats/TypeMismatch2.bpl
index d04a8e9d7..8fa58f413 100644
--- a/Test/floats/TypeMismatch2.bpl
+++ b/Test/floats/TypeMismatch2.bpl
@@ -9,13 +9,13 @@ type double = do;
 
 procedure foo(x : double) returns (r : float)
 {
-  r := 0e128f24e8;
-  r := 1e127f24e8;
+  r := 0x2.0e0f24e8;
+  r := 0x1.000002e0f24e8;
   r := x; //Error
-  r := x * 1e127f24e8; //Error
-  r := x + 1e127f24e8; //Error
-  r := 0e127f24e8 + 0e127f24e8;
-  assert(r == 0e128f24e8);
+  r := x * 0x1.000002e0f24e8; //Error
+  r := x + 0x1.000002e0f24e8; //Error
+  r := 0x1.0e0f24e8 + 0x1.0e0f24e8;
+  assert(r == 0x2.0e0f24e8);
   
   return;
 }
diff --git a/Test/roundingmodes/CorrectTypeConv.bpl b/Test/roundingmodes/CorrectTypeConv.bpl
index 6396b698d..fb6661de6 100644
--- a/Test/roundingmodes/CorrectTypeConv.bpl
+++ b/Test/roundingmodes/CorrectTypeConv.bpl
@@ -20,8 +20,8 @@ procedure main() returns () {
   f32 := TO_FLOAT32_BV32(RNE, 0bv32);
   f64 := TO_FLOAT64_BV64(RTN, 0bv64);
 
-  f32 := TO_FLOAT32_FLOAT64(0e0f53e11);
-  f64 := TO_FLOAT64_FLOAT32(0e0f24e8);
+  f32 := TO_FLOAT32_FLOAT64(0x0.0e0f53e11);
+  f64 := TO_FLOAT64_FLOAT32(0x0.0e0f24e8);
 
   f32 := TO_FLOAT32_FLOAT64(f64);
   f64 := TO_FLOAT64_FLOAT32(f32);
diff --git a/Test/roundingmodes/FloatOperators1.bpl b/Test/roundingmodes/FloatOperators1.bpl
index 101d34a57..c3cc3e331 100644
--- a/Test/roundingmodes/FloatOperators1.bpl
+++ b/Test/roundingmodes/FloatOperators1.bpl
@@ -10,8 +10,8 @@ procedure foo()
   var c : float24e8;
   var d : float24e8;
 
-  a := 0e127f24e8;
-  b := 0e127f24e8;
+  a := 0x1.0e0f24e8;
+  b := 0x1.0e0f24e8;
   c := ADD(RNA, a, b);
   d := ADD(RTP, a, b);
 }
diff --git a/Test/roundingmodes/FloatOperators2.bpl b/Test/roundingmodes/FloatOperators2.bpl
index 7d9857e3f..d81d9a33e 100644
--- a/Test/roundingmodes/FloatOperators2.bpl
+++ b/Test/roundingmodes/FloatOperators2.bpl
@@ -9,7 +9,7 @@ procedure foo()
   var a : float24e8;
   var b : float24e8;
 
-  a := 0e127f24e8;
+  a := 0x1.0e0f24e8;
 
   r := RTN;
   b := SQRT(r, a);
diff --git a/Test/roundingmodes/FloatOpsFixedMode.bpl b/Test/roundingmodes/FloatOpsFixedMode.bpl
index 17ee189c2..d2ae1cc9b 100644
--- a/Test/roundingmodes/FloatOpsFixedMode.bpl
+++ b/Test/roundingmodes/FloatOpsFixedMode.bpl
@@ -9,8 +9,8 @@ procedure foo()
   var a : float24e8;
   var b : float24e8;
 
-  a := 0e127f24e8;
-  b := 0e127f24e8;
+  a := 0x1.0e0f24e8;
+  b := 0x1.0e0f24e8;
 
   b := MUL_RNA(a, b);
 }
diff --git a/Test/roundingmodes/FloatOpsWithoutRoundingMode.bpl b/Test/roundingmodes/FloatOpsWithoutRoundingMode.bpl
index b878431a2..f30cfe3ef 100644
--- a/Test/roundingmodes/FloatOpsWithoutRoundingMode.bpl
+++ b/Test/roundingmodes/FloatOpsWithoutRoundingMode.bpl
@@ -9,8 +9,8 @@ procedure foo()
   var a : float24e8;
   var b : float24e8;
 
-  a := 0e127f24e8;
-  b := 0e127f24e8;
+  a := 0x1.0e0f24e8;
+  b := 0x1.0e0f24e8;
 
   // CHECK: Prover error: line \d+ column \d+: invalid number of arguments to floating point operator
   a := ABS(a);
diff --git a/Test/roundingmodes/RMAttributeInvalid.bpl b/Test/roundingmodes/RMAttributeInvalid.bpl
index a9a64d2cc..1103d0166 100644
--- a/Test/roundingmodes/RMAttributeInvalid.bpl
+++ b/Test/roundingmodes/RMAttributeInvalid.bpl
@@ -8,8 +8,8 @@ procedure foo()
   var a : float24e8;
   var b : float24e8;
 
-  a := 0e127f24e8;
-  b := 0e127f24e8;
+  a := 0x1.0e0f24e8;
+  b := 0x1.0e0f24e8;
   b := ADD(a, b);
-  assert (b == 0e128f24e8);
+  assert (b == 0x2.0e0f24e8);
 }
diff --git a/Test/roundingmodes/UnaffectedOperators.bpl b/Test/roundingmodes/UnaffectedOperators.bpl
index 66632f779..dc96aedaf 100644
--- a/Test/roundingmodes/UnaffectedOperators.bpl
+++ b/Test/roundingmodes/UnaffectedOperators.bpl
@@ -7,7 +7,7 @@ function {:builtin "fp.mul"} MUL(rmode, float24e8, float24e8) returns (float24e8
 function {:builtin "fp.div"} DIV(rmode, float24e8, float24e8) returns (float24e8);
 
 procedure foo(a : float24e8, b : float24e8)
-requires b != 0e0f24e8;
+requires b != 0x0.0e0f24e8;
 {
   var c : float24e8;
   var d : float24e8;