From 49c7d1d0133a789bb8eaa4cc0ff14c5e4493545e Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 7 Jun 2016 10:24:02 -0600 Subject: removed an unnecessary type checking addition --- Test/floats/float3.bpl | 52 +++++++++++++++++++++++++------------------------- 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'Test/floats/float3.bpl') diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl index 34059f80..240c02f3 100644 --- a/Test/floats/float3.bpl +++ b/Test/floats/float3.bpl @@ -1,27 +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; +// 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 -- cgit v1.2.3