diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index fc94305e6b06ccca5d86745f6c58a8768b47e16a..5aecb99741b38304661ebb30982e2f0f9e058b06 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/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
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 77bbb34410117a74c0ebcf763dc156e1917d56b0..37e5908dc093b6461214bde2d3edce7f5bd1a517 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/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))
diff --git a/src/test/resources/regression/verification/purescala/valid/BVDivSemantic.scala b/src/test/resources/regression/verification/purescala/valid/BVDivSemantic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a68525d813e41ae9ae5b0fa82c85c47eaaadebe3
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/BVDivSemantic.scala
@@ -0,0 +1,50 @@
+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)
+
+}
diff --git a/testcases/verification/DivisionSemantic.scala b/testcases/verification/DivisionSemantic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..006fd5364d9186d59ab3d206acc57bf738b9e305
--- /dev/null
+++ b/testcases/verification/DivisionSemantic.scala
@@ -0,0 +1,61 @@
+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)
+
+}