From 53d80ae6818f9fede9acd1eaac42f8129709d412 Mon Sep 17 00:00:00 2001 From: chrishaw Date: Thu, 11 Dec 2014 09:45:08 -0800 Subject: Optimization to nativeType: have EuclideanModulus_sbyte and EuclideanModulus_short call EuclideanModulus_int, not the BigInteger EuclideanModulus. (Same for EuclideanDivision.) --- Binaries/DafnyRuntime.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 83e0563b..dbeb6d0f 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -703,10 +703,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 EuclideanModulus_sbyte(sbyte a, sbyte b) { - return (sbyte)EuclideanModulus(a, b); + return (sbyte)EuclideanModulus_int(a, b); } public static short EuclideanModulus_short(short a, short b) { - return (short)EuclideanModulus(a, b); + return (short)EuclideanModulus_int(a, b); } public static int EuclideanModulus_int(int a, int b) { uint bp = (0 <= b) ? (uint)b : (uint)(unchecked(-b)); -- cgit v1.2.3