From 623a87c132abec61b5c74a6a00a7b162073a6a8d Mon Sep 17 00:00:00 2001
From: boehmes <unknown>
Date: Thu, 27 Sep 2012 17:13:42 +0200
Subject: Boogie: new syntax for integer division and modulus: use div and mod
 instead of / and %

---
 Binaries/DafnyPrelude.bpl | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index ca526173..53e8e86a 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -613,15 +613,15 @@ var $Tick: TickType;
 // -- Arithmetic -------------------------------------------------
 // ---------------------------------------------------------------
 
-// the connection between % and /
-axiom (forall x:int, y:int :: {x % y} {x / y}  x % y == x - x / y * y);
+// the connection between mod and div
+axiom (forall x:int, y:int :: {x mod y} {x div y}  x mod y == x - x div y * y);
 
 // remainder is always Euclidean Modulus.
-axiom (forall x:int, y:int :: {x % y}  0 < y  ==>  0 <= x % y  &&  x % y < y);
-axiom (forall x:int, y:int :: {x % y}  y < 0  ==>  0 <= x % y  &&  x % y < -y);
+axiom (forall x:int, y:int :: {x mod y}  0 < y  ==>  0 <= x mod y  &&  x mod y < y);
+axiom (forall x:int, y:int :: {x mod y}  y < 0  ==>  0 <= x mod y  &&  x mod y < -y);
 
-// the following axiom has some unfortunate matching, but it does state a property about % that
+// the following axiom has some unfortunate matching, but it does state a property about mod that
 // is sometimes useful
-axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b  ==>  a + d <= b);
+axiom (forall a: int, b: int, d: int :: { a mod d, b mod d } 2 <= d && a mod d == b mod d && a < b  ==>  a + d <= b);
 
 // ---------------------------------------------------------------
-- 
cgit v1.2.3