diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2016-07-16 02:49:06 -0600 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2016-07-16 02:49:06 -0600 |
| commit | af8621462cf6b25a6dd29b63ed251629109d6bfb (patch) | |
| tree | 384c961c72fb0cadda51c05db24116896345c494 /Test | |
| parent | 7a0b581cd2e1ec9ce184f195fe0f8d2ea94255c2 (diff) | |
Changed the syntax reading of the float type
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/floats/float0.bpl | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl index b1a240be..1a642835 100644 --- a/Test/floats/float0.bpl +++ b/Test/floats/float0.bpl @@ -1,6 +1,6 @@ // RUN: %boogie -proverWarnings:1 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -procedure foo(x : real) returns (r : float<8, 24>) +procedure foo(x : real) returns (r : float8e24) { r := 15; // Error r := 15.0; // Error |