correct BigInt division and remainder

src/main/scala/leon/purescala/Expressions.scala

@@ -325,6 +325,16 @@ object Expressions {
     require(lhs.getType == IntegerType && rhs.getType == IntegerType)
     val getType = IntegerType
   }
+  /*
+   * Division and Modulo follows Java/Scala semantics. Division corresponds
+   * to / operator on BigInt and Modulo corresponds to %. Note that in
+   * Java/Scala % is rather called remainder and the "mod" operator is also
+   * defined on BigInteger and differs from our Modulo. The "mod" operator
+   * returns an always positive remainder, while our Modulo could return
+   * a negative remainder. The following must hold:
+   *
+   *    Division(x, y) * y + Modulo(x, y) == x
+   */
   case class Division(lhs: Expr, rhs: Expr) extends Expr { 
     require(lhs.getType == IntegerType && rhs.getType == IntegerType)
     val getType = IntegerType

src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala

@@ -644,8 +644,36 @@ abstract class SMTLIBSolver(val context: LeonContext,
       case Plus(a,b) => Ints.Add(toSMT(a), toSMT(b))
       case Minus(a,b) => Ints.Sub(toSMT(a), toSMT(b))
       case Times(a,b) => Ints.Mul(toSMT(a), toSMT(b))
-      case Division(a,b) => Ints.Div(toSMT(a), toSMT(b))
-      case Modulo(a,b) => Ints.Mod(toSMT(a), toSMT(b))
+      case Division(a,b) => {
+        val ar = toSMT(a)
+        val br = toSMT(b)
+
+        val case1 = (
+          Core.And(Ints.LessThan(ar, Ints.NumeralLit(0)), Ints.LessThan(br, Ints.NumeralLit(0))),
+          Ints.Div(Ints.Neg(ar), Ints.Neg(br))
+        )
+        val case2 = (
+          Core.And(Ints.LessThan(ar, Ints.NumeralLit(0)), Ints.GreaterEquals(br, Ints.NumeralLit(0))),
+          Ints.Neg(Ints.Div(Ints.Neg(ar), br))
+        )
+        val case3 = (
+          Core.And(Ints.GreaterEquals(ar, Ints.NumeralLit(0)), Ints.LessThan(br, Ints.NumeralLit(0))),
+          Ints.Div(ar, br)
+        )
+        val case4 = (
+          Core.And(Ints.GreaterEquals(ar, Ints.NumeralLit(0)), Ints.GreaterEquals(br, Ints.NumeralLit(0))),
+          Ints.Div(ar, br)
+        )
+        
+        Core.ITE(case1._1, case1._2,
+          Core.ITE(case2._1, case2._2,
+            Core.ITE(case3._1, case3._2,
+              Core.ITE(case4._1, case4._2, Ints.NumeralLit(0)))))
+      }
+      case Modulo(a,b) => {
+        val q = toSMT(Division(a, b))
+        Ints.Sub(toSMT(a), Ints.Mul(toSMT(b), q))
+      }
       case LessThan(a,b) => a.getType match {
         case Int32Type => FixedSizeBitVectors.SLessThan(toSMT(a), toSMT(b))
         case IntegerType => Ints.LessThan(toSMT(a), toSMT(b))

src/test/resources/regression/verification/purescala/valid/BVDivSemantic.scala

+import leon.lang._
+import leon.collection._
+import leon._
+
+object BVDivSemantics {
+
+  def identity2(x: Int): Boolean = {
+    require(x != -2147483648)
+    -(x / 2) == -x/2
+  } ensuring(res => res)
+
+  def identity3(x: Int): Boolean = {
+    -(x / 2) == x / -2
+  } ensuring(res => res)
+
+  //def identity4(x: Int, y: Int): Boolean = {
+  //  require(y > 0)
+  //  - (x % y) == (-x)%y
+  //} ensuring(res => res)
+
+  def identity5(x: Int): Boolean = {
+    x % 2 == x % -2
+  } ensuring(res => res)
+
+  def identity6(x: Int): Boolean = {
+    require(x != 0)
+    5 % x == 5 % -x
+  } ensuring(res => res)
+
+
+  def basic1(): Boolean = {
+    -3 / 2 == -1
+  } ensuring(res => res)
+  def basic2(): Boolean = {
+    -3 / -2 == 1
+  } ensuring(res => res)
+  def basic3(): Boolean = {
+    3 / -2 == -1
+  } ensuring(res => res)
+  def basic4(): Boolean = {
+    3 % -2 == 1
+  } ensuring(res => res)
+  def basic5(): Boolean = {
+    -3 % -2 == -1
+  } ensuring(res => res)
+  def basic6(): Boolean = {
+    -3 % 2 == -1
+  } ensuring(res => res)
+
+}

testcases/verification/DivisionSemantic.scala

+import leon.lang._
+import leon.collection._
+import leon._
+
+object DivSemantics {
+
+  def identity1(x: BigInt, y: BigInt): Boolean = {
+    require(y > 0)
+    - (x / y) == (-x)/y
+  } ensuring(res => res)
+
+  def identity2(x: BigInt): Boolean = {
+    -(x / 2) == -x/2
+  } ensuring(res => res)
+
+  def identity3(x: BigInt): Boolean = {
+    -(x / 2) == x / -2
+  } ensuring(res => res)
+
+  //def identity4(x: BigInt, y: BigInt): Boolean = {
+  //  require(y > 0)
+  //  - (x % y) == (-x)%y
+  //} ensuring(res => res)
+
+  def identity5(x: BigInt): Boolean = {
+    x % 2 == x % -2
+  } ensuring(res => res)
+
+  def identity6(x: BigInt): Boolean = {
+    require(x != 0)
+    5 % x == 5 % -x
+  } ensuring(res => res)
+
+  def identity1Scoped(x: BigInt, y: BigInt): Boolean = {
+    require(y > 0)
+    val r1 = x / y
+    val r2 = (-x) / y
+    - r1 == r2
+  } ensuring(res => res)
+
+
+  def basic1(): Boolean = {
+    -3 / 2 == -1
+  } ensuring(res => res)
+  def basic2(): Boolean = {
+    -3 / -2 == 1
+  } ensuring(res => res)
+  def basic3(): Boolean = {
+    3 / -2 == -1
+  } ensuring(res => res)
+  def basic4(): Boolean = {
+    3 % -2 == 1
+  } ensuring(res => res)
+  def basic5(): Boolean = {
+    -3 % -2 == -1
+  } ensuring(res => res)
+  def basic6(): Boolean = {
+    -3 % 2 == -1
+  } ensuring(res => res)
+
+}