From 3d182d3d8ad29ca4345114242959cdbbede36f69 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Wed, 13 May 2015 01:55:29 +0200
Subject: [PATCH] updated doc to remove the modulo limitation

---
 doc/limitations.rst | 29 -----------------------------
 1 file changed, 29 deletions(-)

diff --git a/doc/limitations.rst b/doc/limitations.rst
index 374225b0b..8445a4145 100644
--- a/doc/limitations.rst
+++ b/doc/limitations.rst
@@ -15,35 +15,6 @@ the SMT solvers invoked.
 Below we document several cases where we are aware that the
 discrepancy exists and provide suggested workarounds.
 
-Integer Division and Modulo
-^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-On `BigInt` data types, the division operator `/` and
-the modulo operator `%` should only be invoked with positive
-arguments. There are several specific issues.
-
-First, Leon currently does not check for division by zero.
-You can work around this by defining your own division operator
-with the corresponding precondition.
-
-Second, division has rounding-to-zero runtime semantics,
-following Java Virtual Machine and the `BigInt` library
-of Java and Scala, so `(-14)/3 == -4` and, more generally,
-`(-x)/y = -(x/y)`. In general, modulo operator `%` is defined
-so it can be used together with `/`, so that 
-`(x/y)*y + (x % y) == x`. Thus, `(-14) % 3 == -2`.
-
-In contrast, SMT solvers following the SMT-LIB standard use
-rounding to negative infinity, so `(-14)/3 == -5` is a
-theorem, and `(-14) % 3 == 1`. With SMT-LIB semantics, the
-result of modulo `x % y` is non-negative and less than the
-absolute value of `y`.
-
-For the moment we therefore recommend defining your own
-operators with appropriate preconditions. Note that the
-capabilities for automated proofs are limited when the
-second argument of `/` or `%` is not a constant literal.
-
 Out of Memory Errors
 ^^^^^^^^^^^^^^^^^^^^
 
-- 
GitLab