Merge branch 'dfsg_free'

1 files changed, 27 insertions, 0 deletions

diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl
new file mode 100644
index 00000000..507c4127
--- /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 : float24e8;
+	var y : float24e8;
+	var z : float24e8;
+	
+	z := x + y;
+	z := x - y;
+	z := x * y;
+	assume(y != 0e0f24e8);
+	z := x / y;
+	
+	z := (0e127f24e8 + 0e127f24e8 + 0e0f24e8);
+	assert(z == 0e128f24e8);
+	
+	z := 0e128f24e8 - 0e127f24e8;
+	assert(z == 0e127f24e8);
+	
+	z := 0e127f24e8 * 0e127f24e8;
+	assert(z == 0e127f24e8);
+	
+	z := 0e127f24e8 / 0e127f24e8;
+	assert(z == 0e127f24e8);
+	
+	return;
+}
\ No newline at end of file