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 | 2d2475362e0eaaa072464c87dd4a8ae98c0c3d2a (patch) | |
| tree | 67c7df7417df94d3e86b638f0329cf2d6fa6bc9e /Binaries/DafnyPrelude.bpl | |
| parent | 608b5d4feb7f1ecb0172bf18e77e9c0a56365e41 (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/DafnyPrelude.bpl')
| -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);
-
-// ---------------------------------------------------------------
|