diff options
Diffstat (limited to 'Test/floats/float1.bpl')
| -rw-r--r-- | Test/floats/float1.bpl | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl index 2b901c94..d7fc7837 100644 --- a/Test/floats/float1.bpl +++ b/Test/floats/float1.bpl @@ -2,12 +2,12 @@ // RUN: %diff "%s.expect" "%t" procedure foo(x : float24e8) returns (r : float24e8) { - r := 0e1f24e8; - r := 1e0f24e8; + r := 0e128f24e8; + r := 1e127f24e8; r := x; - r := x + 1e0f24e8; - r := 0e0f24e8 + 0e0f24e8; - assert(r == 0e1f24e8); + r := x + 1e127f24e8; + r := 0e127f24e8 + 0e127f24e8; + assert(r == 0e128f24e8); return; }
\ No newline at end of file |