diff options
| author |  chrishaw <unknown> | 2014-12-09 14:54:15 -0800 |
|---|---|---|
| committer | chrishaw <unknown> | 2014-12-09 14:54:15 -0800 |
| commit | 5ceb4c87998c2b0eaa5a6431b717b295e39c2d29 (patch) | |
| tree | 7d88f4ccd09780230177330f22b47dc03994dc8b /Binaries | |
| parent | ac659e1ffa8d3f664daaa9f5394e007ca75cb3d1 (diff) | |
Optimization to nativeType: have EuclideanDivision_sbyte and EuclideanDivision_short call EuclideanDivision_int, not the BigInteger EuclideanDivision. (Same for EuclideanModulus.)
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index a1d9037d..83e0563b 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -638,10 +638,10 @@ namespace Dafny // pre: b != 0
// post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) {
- return (sbyte)EuclideanDivision(a, b);
+ return (sbyte)EuclideanDivision_int(a, b);
}
public static short EuclideanDivision_short(short a, short b) {
- return (short)EuclideanDivision(a, b);
+ return (short)EuclideanDivision_int(a, b);
}
public static int EuclideanDivision_int(int a, int b) {
if (0 <= a) {
|