diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2016-07-19 12:33:21 -0600 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2016-07-19 12:33:21 -0600 |
| commit | 59052004251c655e06951eb4615938259fdf4844 (patch) | |
| tree | 2b11adf8766c1dc4e51a581c4ace79c84b9b4c0c /Test/floats/float7.bpl | |
| parent | 6bf5043aeab0430325c4ccde3e6ca3bd82d96704 (diff) | |
Modified the float tests to match the updated syntax
Diffstat (limited to 'Test/floats/float7.bpl')
| -rw-r--r-- | Test/floats/float7.bpl | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/Test/floats/float7.bpl b/Test/floats/float7.bpl index f330b2ea..c4951681 100644 --- a/Test/floats/float7.bpl +++ b/Test/floats/float7.bpl @@ -1,13 +1,13 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure main() returns () {
- var x : float<11, 53>;
- var y : float<11, 53>;
- var z : float<11, 53>;
- var r : float<11, 53>;
- x := fp<11, 53> (10000000bv64);
- y := x + fp<11, 53>(1bv64);
- z := x - fp<11, 53>(1bv64);
- r := y - z;
- assert r == fp<11, 53> (2bv64);
+// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var x : float53e11; + var y : float53e11; + var z : float53e11; + var r : float53e11; + x := 0e40f53e11; + y := x + 0e0f53e11; + z := x - 0e0f53e11; + r := y - z; + assert r == 0e1f53e11; }
\ No newline at end of file |