diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-08-11 16:07:38 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-08-11 16:07:38 -0700 |
| commit | 8797f054f44d114147562689d80c9970d8ea4f82 (patch) | |
| tree | 6a9e99a6a39126f946c0e7dd55cf0fa03a1a0ca7 /Binaries | |
| parent | 4cbe4583b329a39dee2b4b456758cafbe7e2fa79 (diff) | |
| parent | 08ab990d6f1a188c6cc039d6a2289daf41ff52d3 (diff) | |
Merge
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 6f0cab13..d6bd895a 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -656,6 +656,13 @@ namespace Dafny num = n;
den = d;
}
+ public BigInteger ToBigInteger() {
+ if (0 <= num) {
+ return num / den;
+ } else {
+ return (num - den + 1) / den;
+ }
+ }
/// <summary>
/// Returns values such that aa/dd == a and bb/dd == b.
/// </summary>
|