diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-28 15:19:53 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-28 15:19:53 -0700 |
| commit | a9c6c8fcf205a13c759c6f09e69b01d3b144df94 (patch) | |
| tree | dace58bcf26dcf09e5fd6466b951b0ad4ead5a71 /Binaries | |
| parent | d9f97263c53b3493344a3399daa5402663179b33 (diff) | |
Dafny: removed div/mod axioms, since Boogie now interprets div/mod
Dafny: included FloydCycleDetect again (which had been temporarily commented out)
DafnyExtension: adjusted to Boogie's change in abstract-interpretation support
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 53e8e86a..5530f8a7 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -610,18 +610,3 @@ type TickType; var $Tick: TickType;
// ---------------------------------------------------------------
-// -- Arithmetic -------------------------------------------------
-// ---------------------------------------------------------------
-
-// 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 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 mod that
-// is sometimes useful
-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);
-
-// ---------------------------------------------------------------
|