diff options
Diffstat (limited to 'Test/floats/float3.bpl')
| -rw-r--r-- | Test/floats/float3.bpl | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl index 240c02f3..31de7ca8 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; + var x : float24e8; + var y : float24e8; + var z : float24e8; z := x + y; z := x - y; z := x * y; - assume(y != fp<8, 24>(0bv32)); + assume(y != 0e-128f24e8); z := x / y; - z := (fp<8, 24>(1bv32) + fp<8, 24>(1bv32)) + fp<8, 24>(0bv32); - assert(z == fp<8, 24>(2bv32)); + z := (0e0f24e8 + 0e0f24e8 + 0e-128f24e8); + assert(z == 0e1f24e8); - z := fp<8, 24>(2bv32) - fp<8, 24>(1bv32); - assert(z == fp<8, 24>(1bv32)); + z := 0e1f24e8 - 0e0f24e8; + assert(z == 0e0f24e8); - z := fp(false, 127bv8, 0bv23) * fp(false, 127bv8, 0bv23); - assert(z == fp(false, 127bv8, 0bv23)); + z := 0e0f24e8 * 0e0f24e8; + assert(z == 0e0f24e8); - z := fp<8, 24>(1bv32) / fp<8, 24>(1bv32); - assert(z == fp(false, 127bv8, 0bv23)); + z := 0e0f24e8 / 0e0f24e8; + assert(z == 0e0f24e8); return; }
\ No newline at end of file |