diff --git a/src/main/java/leon/codegen/runtime/BigInt.java b/src/main/java/leon/codegen/runtime/BigInt.java
index 03f12972cb2c89eb92dbe5ef3361baffdee5e00a..83de0fbb4f16ec82843cc64a0bb7eb08f6081148 100644
--- a/src/main/java/leon/codegen/runtime/BigInt.java
+++ b/src/main/java/leon/codegen/runtime/BigInt.java
@@ -35,6 +35,10 @@ public final class BigInt {
     return new BigInt(_underlying.divide(that.underlying()));
   }
 
+  public BigInt rem(BigInt that) {
+    return new BigInt(_underlying.remainder(that.underlying()));
+  }
+
   public BigInt mod(BigInt that) {
     return new BigInt(_underlying.mod(that.underlying()));
   }
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 34cd1a9db20af1ac88323e2022fd0daee7354e0c..1d5dee8b468aaed99dc6742683a28e987c0c5253 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -644,10 +644,11 @@ trait CodeGeneration {
         mkExpr(r, ch)
         ch << InvokeVirtual(BigIntClass, "div", s"(L$BigIntClass;)L$BigIntClass;")
 
+      //Modulo in Leon corresponds to the "rem" operator on java/Scala BigInt
       case Modulo(l, r) =>
         mkExpr(l, ch)
         mkExpr(r, ch)
-        ch << InvokeVirtual(BigIntClass, "mod", s"(L$BigIntClass;)L$BigIntClass;")
+        ch << InvokeVirtual(BigIntClass, "rem", s"(L$BigIntClass;)L$BigIntClass;")
 
       case UMinus(e) =>
         mkExpr(e, ch)
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 81eee7077af71761f1b5d4121bba6ac33a759219..9c441813766e133c095d0608038df991a6ec9224 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -161,6 +161,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
   private def T = BooleanLiteral(true)
   private def F = BooleanLiteral(false)
   private def IL(i : Int) = IntLiteral(i)
+  private def BIL(i : Int) = InfiniteIntegerLiteral(i)
 
   test("Arithmetic") {
     val p = """|object Program {
@@ -195,6 +196,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
       checkComp(e, mkCall("mod", IL(7), IL(-5)), IL(2))
       checkComp(e, mkCall("mod", IL(-7), IL(5)), IL(-2))
       checkComp(e, mkCall("mod", IL(-7), IL(-5)), IL(-2))
+      checkComp(e, mkCall("mod", IL(-1), IL(5)), IL(-1))
 
       // Things that should crash.
       checkError(e, mkCall("div", IL(42), IL(0))) 
@@ -202,6 +204,47 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
     }
   }
 
+  test("BigInt Arithmetic") {
+    val p = """|object Program {
+               |  def plus(x : BigInt, y : BigInt) : BigInt = x + y
+               |  def max(x : BigInt, y : BigInt) : BigInt = if(x >= y) x else y
+               |  def square(i : BigInt) : BigInt = { val j = i; j * i }
+               |  def abs(i : BigInt) : BigInt = if(i < 0) -i else i
+               |  def intSqrt(n : BigInt) : BigInt = intSqrt0(abs(n), 0)
+               |  def intSqrt0(n : BigInt, c : BigInt) : BigInt = {
+               |    val s = square(c+1)
+               |    if(s > n) c else intSqrt0(n, c+1)
+               |  }
+               |  def div(x : BigInt, y : BigInt) : BigInt = (x / y)
+               |  def mod(x : BigInt, y : BigInt) : BigInt = (x % y)
+               |}
+               |""".stripMargin
+
+    implicit val prog = parseString(p)
+    val evaluators = prepareEvaluators
+
+    for(e <- evaluators) {
+      // Some simple math.
+      checkComp(e, mkCall("plus", BIL(60), UMinus(BIL(18))), BIL(42))
+      checkComp(e, mkCall("max", BIL(4), BIL(42)), BIL(42))
+      checkComp(e, mkCall("max", BIL(42), UMinus(BIL(42))), BIL(42))
+      checkComp(e, mkCall("intSqrt", UMinus(BIL(1800))), BIL(42))
+      checkComp(e, mkCall("div", BIL(7), BIL(5)), BIL(1))
+      checkComp(e, mkCall("div", BIL(7), BIL(-5)), BIL(-1))
+      checkComp(e, mkCall("div", BIL(-7), BIL(5)), BIL(-1))
+      checkComp(e, mkCall("div", BIL(-7), BIL(-5)), BIL(1))
+      checkComp(e, mkCall("mod", BIL(7), BIL(5)), BIL(2))
+      checkComp(e, mkCall("mod", BIL(7), BIL(-5)), BIL(2))
+      checkComp(e, mkCall("mod", BIL(-7), BIL(5)), BIL(-2))
+      checkComp(e, mkCall("mod", BIL(-7), BIL(-5)), BIL(-2))
+      checkComp(e, mkCall("mod", BIL(-1), BIL(5)), BIL(-1))
+
+      // Things that should crash.
+      checkError(e, mkCall("div", BIL(42), BIL(0))) 
+      checkError(e, mkCall("mod", BIL(42), BIL(0)))
+    }
+  }
+
   test("Booleans") {
     val p = """|object Program {
                |def and1(x : Boolean, y : Boolean) : Boolean = x && y