finished testing, fixed several minor compiler bugs

50 files changed, 444 insertions, 351 deletions

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index a0ce03a5..3c4cc40a 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -313,7 +313,7 @@ namespace Microsoft.Basetypes
         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 + ")";

+        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() + ")";

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 8161544f..7982f594 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -668,35 +668,7 @@ private class BvBounds : Expr {
    ty = new BasicType(t, SimpleType.Real);

   } else if (la.kind == 98) {

    Get();

-   if (t.val.Length > 5) {

-    switch (Int32.Parse(t.val.Substring(5))) {

-    case 16:

-        ty = new FloatType(t, 5, 11);

-        break;

-    case 32:

-        ty = new FloatType(t, 8, 24);

-        break;

-    case 64:

-        ty = new FloatType(t, 11, 53);

-        break;

-    case 128:

-        ty = new FloatType(t, 15, 113);

-        break;

-    default:

-        SynErr(3);

-        break;

-    }

-   }

-   else {

-    Expect(19); //<

-    Expect(3); //int

-    int exp = Int32.Parse(t.val);

-    Expect(12); //,

-    Expect(3); //int

-    int man = Int32.Parse(t.val);

-    ty = new FloatType(t, exp, man);

-    Expect(20); //>

-   }

+   ty = FType();

   } else if (la.kind == 16) {

 			Get();

 			ty = new BasicType(t, SimpleType.Bool); 

@@ -707,6 +679,39 @@ private class BvBounds : Expr {
 		} else SynErr(101);

 	}

 

+ FloatType FType() {

+   if (t.val.Length > 5) {

+    switch (Int32.Parse(t.val.Substring(5))) {

+     case 16:

+      return new FloatType(t, 5, 11);

+     case 32:

+      return new FloatType(t, 8, 24);

+     case 64:

+      return new FloatType(t, 11, 53);

+     case 128:

+      return new FloatType(t, 15, 113);

+     default:

+      SynErr(3);

+      return new FloatType(t, 0, 0);

+     }

+   }

+   else {

+    try {

+     Expect(19); //<

+     Expect(3); //int

+     int exp = Int32.Parse(t.val);

+     Expect(12); //,

+     Expect(3); //int

+     int man = Int32.Parse(t.val);

+     Expect(20); //>

+     return new FloatType(t, exp, man);

+    }

+    catch (Exception) {

+     return new FloatType(t, 0, 0);

+    }

+   }

+ }

+

 	void Ident(out IToken/*!*/ x) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null);

 		Expect(1);

@@ -1915,8 +1920,13 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
        Get(); //Skip the float token

        if (la.val == "(") {

          Get();

-         Expect(16); //bool

-         negative = Boolean.Parse(t.val);

+         if (la.val == "false")

+           negative = false;

+         else if (la.val == "true")

+           negative = true;

+         else

+           throw new FormatException();

+         Get();

          Expect(12); //,

          BvLit(out exp_val, out exp);

          Expect(12);

@@ -1933,10 +1943,16 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
          sig = Int32.Parse(t.val);

          Expect(20); //>

          Expect(9); //(

-         if (la.kind == 4) {

+         if (la.kind == 1) { //NaN

            Get();

            n = new BigFloat(t.val, exp, sig);

          }

+         else if (la.kind == 74 || la.kind == 75) { //+ or -

+           Get();

+           String s = t.val;

+           Get();

+           n = new BigFloat(s + t.val, exp, sig);

+         }

          else {

            BvLit(out value, out size);

            n = new BigFloat(value.ToString(), exp, sig);

@@ -2194,7 +2210,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		{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,T,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,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,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,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,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,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, 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,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},

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 4982d81e..bc94e253 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -93,7 +93,7 @@ namespace Microsoft.Boogie.SMTLib
         log = log.Replace("\r", "").Replace("\n", " ");

         Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);

       }

-      Console.WriteLine(cmd);

+      //Console.WriteLine(cmd);

       toProver.WriteLine(cmd);

     }

 

diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl
new file mode 100644
index 00000000..b1a240be
--- /dev/null
+++ b/Test/floats/float0.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo(x : real) returns (r : float<8, 24>)
+{
+	r := 15;  // Error
+	r := 15.0;  // Error
+	r := fp(false, 1bv8, 0bv22); // Error
+	r := fp<8, 23>(1bv31); // Error
+	r := x; // Error
+	r := fp<8, 23>(1bv31) + fp<8, 23>(1bv31); // Error
+	r := fp<8, 24>(1bv32) + fp<8, 23>(1bv31); // Error
+	
+	return;
+}
\ No newline at end of file
diff --git a/Test/floats/float0.bpl.expect b/Test/floats/float0.bpl.expect
new file mode 100644
index 00000000..4c934700
--- /dev/null
+++ b/Test/floats/float0.bpl.expect
@@ -0,0 +1,8 @@
+float0.bpl(5,1): Error: mismatched types in assignment command (cannot assign int to float (8 24))

+float0.bpl(6,1): Error: mismatched types in assignment command (cannot assign real to float (8 24))

+float0.bpl(7,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))

+float0.bpl(8,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))

+float0.bpl(9,1): Error: mismatched types in assignment command (cannot assign real to float (8 24))

+float0.bpl(10,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))

+float0.bpl(11,23): Error: invalid argument types (float (8 24) and float (8 23)) to binary operator +

+7 type checking errors detected in float0.bpl

diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl
new file mode 100644
index 00000000..9ed62579
--- /dev/null
+++ b/Test/floats/float1.bpl
@@ -0,0 +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;

+}
\ No newline at end of file
diff --git a/Test/floats/float1.bpl.expect b/Test/floats/float1.bpl.expect
new file mode 100644
index 00000000..6abb715b
--- /dev/null
+++ b/Test/floats/float1.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/floats/float10.bpl b/Test/floats/float10.bpl
new file mode 100644
index 00000000..bf07aec6
--- /dev/null
+++ b/Test/floats/float10.bpl
@@ -0,0 +1,18 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64);
+
+procedure double_range_true() returns () {
+	var x : float64;
+	havoc x;
+	if (x >= TO_FLOAT64_REAL(-1e307) && x <= TO_FLOAT64_REAL(1e307)) {	
+		assert(x==x);
+	}
+}
+
+procedure double_range_false() returns () {
+	var x : float64;
+	havoc x;
+	assert(x==x);
+}
\ No newline at end of file
diff --git a/Test/floats/float10.bpl.expect b/Test/floats/float10.bpl.expect
new file mode 100644
index 00000000..cae8d781
--- /dev/null
+++ b/Test/floats/float10.bpl.expect
@@ -0,0 +1,5 @@
+float10.bpl(17,2): Error BP5001: This assertion might not hold.

+Execution trace:

+    float10.bpl(16,2): anon0

+

+Boogie program verifier finished with 1 verified, 1 error

diff --git a/Test/floats/float11.bpl b/Test/floats/float11.bpl
new file mode 100644
index 00000000..424c5a2d
--- /dev/null
+++ b/Test/floats/float11.bpl
@@ -0,0 +1,22 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

+

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);

+

+procedure main() returns () {

+	var tick : float32;

+	var time : float32;

+	var i: int;

+	

+	tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10);

+	time := TO_FLOAT32_INT(0);

+	

+	i := 0;

+	while (i < 10)

+	{

+		time := time + tick;

+		i := i + 1;

+	}

+	assert time == TO_FLOAT32_INT(1);

+}
\ No newline at end of file
diff --git a/Test/floats/float11.bpl.expect b/Test/floats/float11.bpl.expect
new file mode 100644
index 00000000..19e55fef
--- /dev/null
+++ b/Test/floats/float11.bpl.expect
@@ -0,0 +1,7 @@
+..\Test\floats\float11.bpl(21,2): Error BP5001: This assertion might not hold.

+Execution trace:

+    ..\Test\floats\float11.bpl(12,7): anon0

+    ..\Test\floats\float11.bpl(16,2): anon3_LoopHead

+    ..\Test\floats\float11.bpl(16,2): anon3_LoopDone

+

+Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/floats/float12.bpl b/Test/floats/float12.bpl
new file mode 100644
index 00000000..349abb41
--- /dev/null
+++ b/Test/floats/float12.bpl
@@ -0,0 +1,16 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64);
+
+procedure main() returns () {
+	var x : float64;
+	var y : float32;
+	
+	x := TO_FLOAT64_REAL(1e20)+TO_FLOAT64_INT(1);
+	y := TO_FLOAT32_FLOAT64(x);
+	assert x != TO_FLOAT64_FLOAT32(y);
+}
\ No newline at end of file
diff --git a/Test/floats/float12.bpl.expect b/Test/floats/float12.bpl.expect
new file mode 100644
index 00000000..6abb715b
--- /dev/null
+++ b/Test/floats/float12.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl
new file mode 100644
index 00000000..4fe25140
--- /dev/null
+++ b/Test/floats/float13.bpl
@@ -0,0 +1,23 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64);
+
+procedure main() returns () {
+	var x : float64;
+	var y : float64;
+
+	havoc x;
+	assume(x >= TO_FLOAT64_INT(0) && x <= TO_FLOAT64_INT(10));
+
+	y := x*x - x;
+	if (y >= TO_FLOAT64_INT(0)) {
+		y := x / TO_FLOAT64_INT(10);
+	}
+	else {
+		y := x*x + TO_FLOAT64_INT(2);
+	}
+	
+	assert(y >= TO_FLOAT64_INT(0) && y <= TO_FLOAT64_INT(105));
+}
\ No newline at end of file
diff --git a/Test/floats/float14.bpl b/Test/floats/float14.bpl
new file mode 100644
index 00000000..46c1b07d
--- /dev/null
+++ b/Test/floats/float14.bpl
@@ -0,0 +1,17 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64);
+
+procedure main() returns () {
+	var x : float64;
+	var y : float64;
+	var r : float64;
+	
+	x := TO_FLOAT64_INT(77617);
+	y := TO_FLOAT64_INT(33096);
+	r := y*y*y*y*y*y * TO_FLOAT64_REAL(333.75) + x*x * (x*x*y*y*TO_FLOAT64_INT(11) - y*y*y*y*y*y - y*y*y*y * TO_FLOAT64_INT(121) - TO_FLOAT64_INT(2)) + y*y*y*y*y*y*y*y * TO_FLOAT64_REAL(5.5) + x / (y*TO_FLOAT64_INT(2));
+	
+	assert(r >= TO_FLOAT64_INT(0));
+}
\ No newline at end of file
diff --git a/Test/floats/test5.bpl b/Test/floats/float15.bpl
index 7536f8fd..7536f8fd 100644
--- a/Test/floats/test5.bpl
+++ b/Test/floats/float15.bpl
diff --git a/Test/floats/test6.bpl b/Test/floats/float16.bpl
index 6bef1137..6bef1137 100644
--- a/Test/floats/test6.bpl
+++ b/Test/floats/float16.bpl
diff --git a/Test/floats/test7.bpl b/Test/floats/float17.bpl
index 8e07878d..8e07878d 100644
--- a/Test/floats/test7.bpl
+++ b/Test/floats/float17.bpl
diff --git a/Test/floats/test8.bpl b/Test/floats/float18.bpl
index 7e78e206..7e78e206 100644
--- a/Test/floats/test8.bpl
+++ b/Test/floats/float18.bpl
diff --git a/Test/floats/test9.bpl b/Test/floats/float19.bpl
index c3a42e6b..c3a42e6b 100644
--- a/Test/floats/test9.bpl
+++ b/Test/floats/float19.bpl
diff --git a/Test/floats/float2.bpl b/Test/floats/float2.bpl
new file mode 100644
index 00000000..1a4d02cd
--- /dev/null
+++ b/Test/floats/float2.bpl
@@ -0,0 +1,15 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

+procedure foo(x : float16) returns(r : float32) {

+	var y : float64;

+	var z : float128;

+	

+	r := x; // Error

+	r := y; // Error

+	r := z; // Error

+	y := x; // Error

+	y := z; // Error

+	z := x; // Error

+

+	return;

+}
\ No newline at end of file
diff --git a/Test/floats/float2.bpl.expect b/Test/floats/float2.bpl.expect
new file mode 100644
index 00000000..62348741
--- /dev/null
+++ b/Test/floats/float2.bpl.expect
@@ -0,0 +1,7 @@
+float2.bpl(7,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (8 24))

+float2.bpl(8,1): Error: mismatched types in assignment command (cannot assign float (11 53) to float (8 24))

+float2.bpl(9,1): Error: mismatched types in assignment command (cannot assign float (15 113) to float (8 24))

+float2.bpl(10,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (11 53))

+float2.bpl(11,1): Error: mismatched types in assignment command (cannot assign float (15 113) to float (11 53))

+float2.bpl(12,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (15 113))

+6 type checking errors detected in float2.bpl

diff --git a/Test/floats/test20.bpl b/Test/floats/float20.bpl
index 57c605fd..57c605fd 100644
--- a/Test/floats/test20.bpl
+++ b/Test/floats/float20.bpl
diff --git a/Test/floats/float21.bpl b/Test/floats/float21.bpl
new file mode 100644
index 00000000..5fad5859
--- /dev/null
+++ b/Test/floats/float21.bpl
@@ -0,0 +1,35 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

+

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);

+

+procedure main() returns () {

+	var x : float32;

+	var y : float32;

+	var z : float32;

+	

+	havoc x;

+	assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));

+	

+	if (x != TO_FLOAT32_INT(0)) {

+		y := x * x;

+		assert(y != TO_FLOAT32_INT(0));

+		z := TO_FLOAT32_INT(1) / y;

+	}

+}

+

+procedure main() returns () {

+	var x : float32;

+	var y : float32;

+	var z : float32;

+	

+	havoc x;

+	assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));

+	

+	if (x <= TO_FLOAT32_REAL(-1e-20) || x >= TO_FLOAT32_REAL(1e-20)) {

+		y := x * x;

+		assert(y != TO_FLOAT32_INT(0));

+		z := TO_FLOAT32_INT(1) / y;

+	}

+}
\ No newline at end of file
diff --git a/Test/floats/test14.bpl b/Test/floats/float22.bpl
index 1505c361..1505c361 100644
--- a/Test/floats/test14.bpl
+++ b/Test/floats/float22.bpl
diff --git a/Test/floats/test16.bpl b/Test/floats/float23.bpl
index 69ae243d..69ae243d 100644
--- a/Test/floats/test16.bpl
+++ b/Test/floats/float23.bpl
diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl
new file mode 100644
index 00000000..34059f80
--- /dev/null
+++ b/Test/floats/float3.bpl
@@ -0,0 +1,27 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

+procedure main() returns () {

+	var x : float32;

+	var y : float32;

+	var z : float32;

+	

+	z := x + y;

+	z := x - y;

+	z := x * y;

+	assume(y != fp<8, 24>(0bv32));

+	z := x / y;

+	

+	z := (fp<8, 24>(1bv32) + fp<8, 24>(1bv32)) + fp<8, 24>(0bv32);

+	assert(z == fp<8, 24>(2bv32));

+	

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

+	assert(z == fp<8, 24>(1bv32));

+	

+	z := fp(false, 127bv8, 0bv23) * fp(false, 127bv8, 0bv23);

+	assert(z == fp(false, 127bv8, 0bv23));

+	

+	z := fp<8, 24>(1bv32) / fp<8, 24>(1bv32);

+	assert(z == fp(false, 127bv8, 0bv23));

+	

+	return;

+}
\ No newline at end of file
diff --git a/Test/floats/float3.bpl.expect b/Test/floats/float3.bpl.expect
new file mode 100644
index 00000000..6abb715b
--- /dev/null
+++ b/Test/floats/float3.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl
new file mode 100644
index 00000000..7bb24250
--- /dev/null
+++ b/Test/floats/float4.bpl
@@ -0,0 +1,11 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

+procedure foo() returns (r : float32) {

+	r := fp<8, 24>(NaN);

+	r := fp<8, 24>(+oo);

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

+	r := fp<8, 24>(+zero);

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

+	

+	return;

+}
\ No newline at end of file
diff --git a/Test/floats/float4.bpl.expect b/Test/floats/float4.bpl.expect
new file mode 100644
index 00000000..6abb715b
--- /dev/null
+++ b/Test/floats/float4.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/floats/float5.bpl b/Test/floats/float5.bpl
new file mode 100644
index 00000000..fd630394
--- /dev/null
+++ b/Test/floats/float5.bpl
@@ -0,0 +1,24 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

+

+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_INT(int) returns (float<8, 23>);

+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_REAL(real) returns (float<8, 23>);

+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV31(bv31) returns (float<8, 23>);

+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV32(bv32) returns (float<8, 23>);

+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_FLOAT824(float<8, 24>) returns (float<8, 23>);

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT823(float<8, 23>) returns (float<8, 24>);

+

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

+	r := TO_FLOAT823_INT(5); // Error

+	r := TO_FLOAT823_REAL(5.0); // Error

+	r := TO_FLOAT823_BV31(0bv31); // Error

+	r := TO_FLOAT823_BV32(0bv32); // Error

+	r := TO_FLOAT823_FLOAT824(fp<8, 24>(1bv32)); // Error

+	r := TO_FLOAT824_FLOAT823(fp<8, 24>(1bv32)); // Error

+	r := TO_FLOAT824_FLOAT823(fp<8, 23>(1bv31));

+	

+	r := TO_FLOAT823_FLOAT824(x); // Error

+	r := TO_FLOAT824_FLOAT823(x); // Error

+	

+	return;

+}
\ No newline at end of file
diff --git a/Test/floats/float5.bpl.expect b/Test/floats/float5.bpl.expect
new file mode 100644
index 00000000..6c0b86af
--- /dev/null
+++ b/Test/floats/float5.bpl.expect
@@ -0,0 +1,9 @@
+float5.bpl(12,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))

+float5.bpl(13,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))

+float5.bpl(14,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))

+float5.bpl(15,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))

+float5.bpl(16,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))

+float5.bpl(17,42): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float (8 24) (expected: float (8 23))

+float5.bpl(20,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))

+float5.bpl(21,27): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float (8 24) (expected: float (8 23))

+8 type checking errors detected in float5.bpl

diff --git a/Test/floats/float6.bpl b/Test/floats/float6.bpl
new file mode 100644
index 00000000..fe0eab0e
--- /dev/null
+++ b/Test/floats/float6.bpl
@@ -0,0 +1,50 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

+

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_INT(int) returns (float<8, 24>);

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_REAL(real) returns (float<8, 24>);

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_BV32(bv32) returns (float<8, 24>);

+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT1153_BV64(bv64) returns (float<11, 53>);

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT32(float32) returns (float<8, 24>);  //Should just be an identity function

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT824(float<8, 24>) returns (float32); //Should just be an identity function

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32);

+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64);

+

+procedure main() returns () {

+	var i : int;

+	var r : real;

+	var f824 : float<8, 24>;

+	var f32 : float32;

+	var f1153 : float<11, 53>;

+	var f64 : float64;

+	

+	f824 := TO_FLOAT824_INT(5);

+	f32 := TO_FLOAT824_INT(5);

+	f824 := TO_FLOAT824_REAL(5.0);

+	f32 := TO_FLOAT824_REAL(5.0);

+	

+	f824 := TO_FLOAT824_BV32(0bv32);

+	f32 := TO_FLOAT824_BV32(0bv32);

+	f1153 := TO_FLOAT1153_BV64(0bv64);

+	f64 := TO_FLOAT1153_BV64(0bv64);

+	

+	f824 := TO_FLOAT824_FLOAT32(fp<8, 24>(0bv32));

+	f32 := TO_FLOAT32_FLOAT824(fp<8, 24>(0bv32));

+	f824 := TO_FLOAT32_FLOAT64(fp<11, 53>(0bv32));

+	f32 := TO_FLOAT32_FLOAT64(fp<11, 53>(0bv32));

+	f1153 := TO_FLOAT64_FLOAT32(fp<8, 24>(0bv32));

+	f64 := TO_FLOAT64_FLOAT32(fp<8, 24>(0bv32));

+	

+	f824 := TO_FLOAT824_INT(5);

+	f32 := TO_FLOAT32_FLOAT824(f824);

+	assert(f32 == f824);

+	

+	f32 := TO_FLOAT824_INT(5);

+	f824 := TO_FLOAT824_FLOAT32(f32);

+	assert(f32 == f824);

+	

+	f32 := TO_FLOAT32_FLOAT64(f64);

+	f64 := TO_FLOAT64_FLOAT32(f32);

+	

+	return;

+}
\ No newline at end of file
diff --git a/Test/floats/float6.bpl.expect b/Test/floats/float6.bpl.expect
new file mode 100644
index 00000000..6abb715b
--- /dev/null
+++ b/Test/floats/float6.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/floats/test1.bpl b/Test/floats/float7.bpl
index e893e098..f330b2ea 100644
--- a/Test/floats/test1.bpl
+++ b/Test/floats/float7.bpl
@@ -1,13 +1,13 @@
-//Translation from addsub_double_exact.c
-//Should Verify
-procedure main() returns () {
-	var x : float<11, 53>;
-	var y : float<11, 53>;
-	var z : float<11, 53>;
-	var r : float<11, 53>;
-	x := fp<11, 53> (10000000bv64);
-	y := x + fp<11, 53>(1bv64);
-	z := x - fp<11, 53>(1bv64);
-	r := y - z;
-	assert r == fp<11, 53> (2bv64);
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

+procedure main() returns () {

+	var x : float<11, 53>;

+	var y : float<11, 53>;

+	var z : float<11, 53>;

+	var r : float<11, 53>;

+	x := fp<11, 53> (10000000bv64);

+	y := x + fp<11, 53>(1bv64);

+	z := x - fp<11, 53>(1bv64);

+	r := y - z;

+	assert r == fp<11, 53> (2bv64);

 }
\ No newline at end of file
diff --git a/Test/floats/float7.bpl.expect b/Test/floats/float7.bpl.expect
new file mode 100644
index 00000000..6abb715b
--- /dev/null
+++ b/Test/floats/float7.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/floats/test3.bpl b/Test/floats/float8.bpl
index 67c6ba48..78c11a2b 100644
--- a/Test/floats/test3.bpl
+++ b/Test/floats/float8.bpl
@@ -1,13 +1,13 @@
-//Translation from addsub_float_inexact.c
-//Should give an error
-procedure main() returns () {
-	var x : float32;
-	var y : float32;
-	var z : float32;
-	var r : float32;
-	x := fp<8, 24>(3221225472bv32);
-	y := x + fp<8, 24>(1bv32);
-	z := x - fp<8, 24>(1bv32);
-	r := y - z;
-	assert r == fp<8, 24>(2bv32);
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

+procedure main() returns () {

+	var x : float32;

+	var y : float32;

+	var z : float32;

+	var r : float32;

+	x := fp<8, 24>(3221225472bv32);

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

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

+	r := y - z;

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

 }
\ No newline at end of file
diff --git a/Test/floats/float8.bpl.expect b/Test/floats/float8.bpl.expect
new file mode 100644
index 00000000..426c21e0
--- /dev/null
+++ b/Test/floats/float8.bpl.expect
@@ -0,0 +1,5 @@
+float8.bpl(12,2): Error BP5001: This assertion might not hold.

+Execution trace:

+    float8.bpl(8,4): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/floats/test2.bpl b/Test/floats/float9.bpl
index d78c339d..cb4f3afd 100644
--- a/Test/floats/test2.bpl
+++ b/Test/floats/float9.bpl
@@ -1,17 +1,17 @@
-//Translation from addsub_float_exact.c
-//Should Verify
-
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);
-
-procedure main() returns () {
-	var x : float32;
-	var y : float32;
-	var z : float32;
-	var r : float32;
-	x := TO_FLOAT32_REAL(1e7);
-	y := x + TO_FLOAT32_INT(1);
-	z := x - TO_FLOAT32_INT(1);
-	r := y - z;
-	assert r == TO_FLOAT32_INT(2);
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"

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

+

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);

+

+procedure main() returns () {

+	var x : float32;

+	var y : float32;

+	var z : float32;

+	var r : float32;

+	x := TO_FLOAT32_REAL(1e7);

+	y := x + TO_FLOAT32_INT(1);

+	z := x - TO_FLOAT32_INT(1);

+	r := y - z;

+	assert r == TO_FLOAT32_INT(2);

 }
\ No newline at end of file
diff --git a/Test/floats/float9.bpl.expect b/Test/floats/float9.bpl.expect
new file mode 100644
index 00000000..6abb715b
--- /dev/null
+++ b/Test/floats/float9.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/floats/modpath.py b/Test/floats/modpath.py
new file mode 100644
index 00000000..90707701
--- /dev/null
+++ b/Test/floats/modpath.py
@@ -0,0 +1,13 @@
+import sys

+

+f = open(sys.argv[1], 'r')

+to_write = ""

+

+for i in f:

+	to_write += i.replace("..\\Test\\floats\\", "")

+	

+f.close()

+

+f = open(sys.argv[1], 'w')

+

+f.write(to_write)
\ No newline at end of file
diff --git a/Test/floats/test10.bpl b/Test/floats/test10.bpl
deleted file mode 100644
index 566f7a56..00000000
--- a/Test/floats/test10.bpl
+++ /dev/null
@@ -1,20 +0,0 @@
-//Translation from loop.c
-//Should return an error?  (The real case does as well...)
-
-procedure main() returns () {
-	var x : float;
-	var y : float;
-	var z : float;
-	
-	x := fp(1);
-	y := fp(10000000);
-	z := fp(42);
-	
-	while (x < y) {
-		x := x + fp(1);
-		y := y - fp(1);
-		z := z + fp(1);
-	}
-	
-	assert(z >= fp(0) && z <= fp(10000000));
-}
\ No newline at end of file
diff --git a/Test/floats/test11.bpl b/Test/floats/test11.bpl
deleted file mode 100644
index cee3e36e..00000000
--- a/Test/floats/test11.bpl
+++ /dev/null
@@ -1,55 +0,0 @@
-//Translation from interpolation.c

-//Should Verify

-//Returns inconclusive?  What does that mean?

-

-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);

-procedure main() returns () {

-	var i : int;

-	var z : float32;

-	var t : float32;

-	var min : [int] float32;

-	var max : [int] float32;

-	

-	min[0] := TO_FLOAT32_INT(5);

-	min[1] := TO_FLOAT32_INT(10);

-	min[2] := TO_FLOAT32_INT(12);

-	min[3] := TO_FLOAT32_INT(30);

-	min[4] := TO_FLOAT32_INT(150);

-	

-	max[0] := TO_FLOAT32_INT(10);

-	max[1] := TO_FLOAT32_INT(12);

-	max[2] := TO_FLOAT32_INT(30);

-	max[3] := TO_FLOAT32_INT(150);

-	max[4] := TO_FLOAT32_INT(300);

-	

-	havoc t;

-	assume(t >= min[0] && t <= max[4]);

-	

-	i := 0;

-	//while (i < 5) {

-		//if (t <= max[i]) {

-			//break;

-		//}

-		//i := i + 1;

-	//}

-	

-	if (t > max[0]) { //1

-		i := i + 1;

-	}

-	if (t > max[1]) { //2

-		i := i + 1;

-	}

-	if (t > max[2]) { //3

-		i := i + 1;

-	}

-	if (t > max[3]) { //4

-		i := i + 1;

-	}

-	if (t > max[4]) { //5

-		i := i + 1;

-	}

-	

-	z := (t - min[i]) / (max[i] - min[i]);

-	

-	assert(z >= TO_FLOAT32_INT(0) && z <= TO_FLOAT32_INT(1));

-}
\ No newline at end of file
diff --git a/Test/floats/test12.bpl b/Test/floats/test12.bpl
deleted file mode 100644
index c733b9f4..00000000
--- a/Test/floats/test12.bpl
+++ /dev/null
@@ -1,43 +0,0 @@
-//Translation from inv_Newton.c

-//Should Verify

-//Unfinished code!

-

-procedure inv(float(11 53)) returns(float(11 53)) {

-	var z : float(11 53);

-	var t : float(11 53);

-	var t : float(11 53);

-	

-	

-}

-

-procedure main() returns () {

-	var t : float(11 53);

-	var t : float(11 53);

-	

-	min[0] := fp(5);

-	min[1] := fp(10);

-	min[2] := fp(12);

-	min[3] := fp(30);

-	min[4] := fp(150);

-	

-	max[0] := fp(10);

-	max[1] := fp(12);

-	max[2] := fp(30);

-	max[3] := fp(150);

-	max[4] := fp(300);

-	

-	havoc t;

-	assume(t >= min[0] && t <= max[4]);

-	

-	i := 0;

-	while (i < 5) {

-		if (t <= max[i]) {

-			break;

-		}

-		i := i + 1;

-	}

-	

-	z := (t - min[i]) / (max[i] - min[i]);

-	

-	assert(z >= fp(0) && z <= fp(1));

-}
\ No newline at end of file
diff --git a/Test/floats/test13.bpl b/Test/floats/test13.bpl
deleted file mode 100644
index e5402539..00000000
--- a/Test/floats/test13.bpl
+++ /dev/null
@@ -1,19 +0,0 @@
-//Translation from inv_square_false-unreach-call.c

-//Should return an error (without crashing)

-

-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);

-

-procedure main() returns () {

-	var x : float32;

-	var y : float32;

-	var z : float32;

-	

-	havoc x;

-	assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));

-	

-	if (x != TO_FLOAT32_INT(0)) {

-		y := x * x;

-		assert(y != TO_FLOAT32_INT(0));

-		z := TO_FLOAT32_INT(1) / y;

-	}

-}
\ No newline at end of file
diff --git a/Test/floats/test15.bpl b/Test/floats/test15.bpl
deleted file mode 100644
index 1dc549ac..00000000
--- a/Test/floats/test15.bpl
+++ /dev/null
@@ -1,24 +0,0 @@
-//Translation from Muller_Kahan.c

-//Should Verify

-//NOTE:  (fp(....)) causes a compiler error!

-//FAILS!  Heavily...

-

-procedure main() returns () {

-	var x0 : float(11 53);

-	var x1 : float(11 53);

-	var x2 : float(11 53);

-	var i : int;

-	

-	x0 := fp(11 11 53) / fp(2 11 53);

-	x1 := fp(61 11 53) / fp(11 11 53);

-	i := 0;

-	while (i < 100) {

-		x2 := fp(1130 11 53) - fp(3000 11 53) / x0;

-		x2 := fp(111 11 53) - x2 / x1;

-		x0 := x1;

-		x1 := x2;

-		i := i + 1;

-	}

-	

-	assert(x0 >= fp(99 11 53) && x0 <= fp(101 11 53));

-}
\ No newline at end of file
diff --git a/Test/floats/test17.bpl b/Test/floats/test17.bpl
deleted file mode 100644
index caa1fa74..00000000
--- a/Test/floats/test17.bpl
+++ /dev/null
@@ -1,11 +0,0 @@
-//Translation from nan_double_range_true-unreach-call.c

-//Should verify

-//Uggghhhh, should I add support for e?

-

-procedure main() returns () {

-	var x : float(11 53);

-	havoc x;

-	if (x >= fp(-100000000000000000000000000 11 53) && x <= fp(100000000000000000000000000 11 53)) {	

-		assert(x==x);

-	}

-}
\ No newline at end of file
diff --git a/Test/floats/test18.bpl b/Test/floats/test18.bpl
deleted file mode 100644
index 71eb5286..00000000
--- a/Test/floats/test18.bpl
+++ /dev/null
@@ -1,36 +0,0 @@
-//Translation from rlim_exit.c

-//Should verify

-//Unary - unsupported float operations (on my end)...

-

-procedure main() returns () {

-	var X : float;

-	var Y : float;

-	var S : float;

-	var R : float;

-	var D : float;

-	var i : int;

-	

-	Y := fp(0);

-	

-	i := 0;

-	while (i < 100000) {

-		havoc X;

-		havoc D;

-		assume(X >= fp(-128) && X <= fp(128));

-		assume(D >= fp(0) && D <= fp(16));

-		

-		S := Y;

-		Y := X;

-		R := X - S;

-		if (R <= fp(0)-D) {

-			Y := S - D;

-		}

-		else if(R >= D) {

-			Y := S + D;

-		}

-		

-		i := i + 1;

-	}

-	

-	assert(Y >= fp(-129) && Y <= fp(129));

-}
\ No newline at end of file
diff --git a/Test/floats/test19.bpl b/Test/floats/test19.bpl
deleted file mode 100644
index f00d8a2b..00000000
--- a/Test/floats/test19.bpl
+++ /dev/null
@@ -1,36 +0,0 @@
-//Translation from flim_invariant.c

-//Should verify

-//Unary - unsupported float operations (on my end)...

-

-procedure main() returns () {

-	var X : float;

-	var Y : float;

-	var S : float;

-	var R : float;

-	var D : float;

-	var i : int;

-	

-	Y := fp(0);

-	

-	i := 0;

-	while (i < 100000) {

-		havoc X;

-		havoc D;

-		assume(X >= fp(-128) && X <= fp(128));

-		assume(D >= fp(0) && D <= fp(16));

-		

-		S := Y;

-		Y := X;

-		R := X - S;

-		if (R <= fp(0)-D) {

-			Y := S - D;

-		}

-		else if(R >= D) {

-			Y := S + D;

-		}

-		

-		assert(Y >= fp(-129) && Y <= fp(129));

-		

-		i := i + 1;

-	}

-}
\ No newline at end of file
diff --git a/Test/floats/test4.bpl b/Test/floats/test4.bpl
deleted file mode 100644
index a31aa215..00000000
--- a/Test/floats/test4.bpl
+++ /dev/null
@@ -1,32 +0,0 @@
-//Translation from drift_tenth.c
-//Should Fail
-
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);
-
-procedure main() returns () {
-	var tick : float32;
-	var time : float32;
-	var i: int;
-	
-	tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10);
-	time := TO_FLOAT32_INT(0);
-	
-	//i := 0;
-	//while (i < 10)
-	//{
-	//	time := time + tick;
-	//	i := i + 1;
-	//}
-	time := time + tick;//1
-	time := time + tick;//2
-	time := time + tick;//3
-	time := time + tick;//4
-	time := time + tick;//5
-	time := time + tick;//6
-	time := time + tick;//7
-	time := time + tick;//8
-	time := time + tick;//9
-	time := time + tick;//10
-	assert time == TO_FLOAT32_INT(1);
-}
\ No newline at end of file