diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 70d8091b2df531781e6816557eaadd7331827837..415f4edaa8b63edd319a696c7dc9042e75692cda 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -49,6 +49,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
             case e @ Error(_, "Match is non-exhaustive") =>
               (e, VCKinds.ExhaustiveMatch, BooleanLiteral(false))
 
+
             case e @ Error(_, _) =>
               (e, VCKinds.Assert, BooleanLiteral(false))
 
@@ -57,6 +58,8 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
                 VCKinds.MapUsage
               } else if (err.startsWith("Array ")) {
                 VCKinds.ArrayUsage
+              } else if (err.startsWith("Division ")) {
+                VCKinds.DivisionByZero
               } else {
                 VCKinds.Assert
               }
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 8d0645e9ba56198a7a71c38486ac60bef270dab5..3e371b3bc7323c079628ba27d1dc96af3569757a 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -30,6 +30,18 @@ object InjectAsserts extends LeonPhase[Program, Program] {
           Some(Assert(indexUpTo(i, ArrayLength(a)), Some("Array index out of range"), e).setPos(e))
         case e @ MapGet(m,k) =>
           Some(Assert(MapIsDefinedAt(m, k), Some("Map undefined at this index"), e).setPos(e))
+
+        case e @ Division(_, d)  =>
+          Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+                      Some("Division by zero"),
+                      e
+                     ).setPos(e))
+        case e @ BVDivision(_, d)  =>
+          Some(Assert(Not(Equals(d, IntLiteral(0))),
+                      Some("Division by zero"),
+                      e
+                     ).setPos(e))
+
         case _ =>
           None
       }) 
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 46e255d9caa2c8d5edf84442ef725eb9f70faca9..890a16d065c7a142aa3aae5e67aaab4cace46faa 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -34,6 +34,7 @@ object VCKinds {
   case object ExhaustiveMatch extends VCKind("match exhaustiveness", "match.")
   case object MapUsage        extends VCKind("map usage", "map use")
   case object ArrayUsage      extends VCKind("array usage", "arr. use")
+  case object DivisionByZero  extends VCKind("division by zero", "div 0")
 }
 
 case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option[Long]) {
diff --git a/src/test/resources/regression/verification/purescala/invalid/BVDivision.scala b/src/test/resources/regression/verification/purescala/invalid/BVDivision.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a2572db84870fa38ab5f4f6a924ddbaa1641d47f
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/BVDivision.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object BVDivision {
+
+  def divByZero(x: Int): Boolean = {
+    (x / 0 == 10)
+  }
+  
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/Division.scala b/src/test/resources/regression/verification/purescala/invalid/Division.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6b505a7732f6a6b0126e2c4b4106c16426069823
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/Division.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object Division {
+
+  def divByZero(x: BigInt): Boolean = {
+    (x / BigInt(0) == BigInt(10))
+  }
+  
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/BVDivision.scala b/src/test/resources/regression/verification/purescala/valid/BVDivision.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2121f416e3fe776c50f0502c6439c55832ad0cc0
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/BVDivision.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object BVDivision {
+
+  def noDivByZero(x: Int): Boolean = {
+    (x / 10 == 10)
+  }
+  
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/Division.scala b/src/test/resources/regression/verification/purescala/valid/Division.scala
new file mode 100644
index 0000000000000000000000000000000000000000..49337b86d39a4a0199999d9380ef49c9d56fd569
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Division.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object Division {
+
+  def noDivByZero(x: BigInt): Boolean = {
+    (x / BigInt(10) == BigInt(10))
+  }
+  
+}