From 5ceb4c87998c2b0eaa5a6431b717b295e39c2d29 Mon Sep 17 00:00:00 2001 From: chrishaw Date: Tue, 9 Dec 2014 14:54:15 -0800 Subject: Optimization to nativeType: have EuclideanDivision_sbyte and EuclideanDivision_short call EuclideanDivision_int, not the BigInteger EuclideanDivision. (Same for EuclideanModulus.) --- Binaries/DafnyRuntime.cs | 4 ++-- 1 file 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) { -- cgit v1.2.3