Dafny: Dafny now uses the Euclidean definition of division. (Verifier and runtime.)

1 files changed, 3 insertions, 3 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 94a8833a..dc152185 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -373,12 +373,12 @@ var $Tick: TickType;
 // the connection between % and /

 axiom (forall x:int, y:int :: {x % y} {x / y}  x % y == x - x / y * y);

 

-// sign of denominator determines sign of remainder

+// 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  ==>  y < x % y  &&  x % y <= 0);

+axiom (forall x:int, y:int :: {x % y}  y < 0  ==>  0 <= x % y  &&  x % y < -y);

 

 // the following axiom has some unfortunate matching, but it does state a property about % that

-// is sometime useful

+// 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);

 

 // ---------------------------------------------------------------