finished testing, fixed several minor compiler bugs

1 files changed, 23 insertions, 0 deletions

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