diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index fae6329c855c29d29fdc99cd8e300f19f2d21c14..2710b399445de20145770a14bfcd47b364143c4b 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -62,6 +62,12 @@ object InjectAsserts extends LeonPhase[Program, Program] {
                       e
                      ).setPos(e))
 
+        case e @ RealDivision(_, d)  =>
+          Some(Assert(Not(Equals(d, RealLiteral(0))),
+                      Some("Division by zero"),
+                      e
+                     ).setPos(e))
+
         case _ =>
           None
       }) 
diff --git a/src/test/resources/regression/verification/purescala/invalid/RealDivisionByZero.scala b/src/test/resources/regression/verification/purescala/invalid/RealDivisionByZero.scala
new file mode 100644
index 0000000000000000000000000000000000000000..418fbb9e81cb441518a616c506b467bfe912635e
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/RealDivisionByZero.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object RealDivisionByZero {
+
+  def divByZero(x: Real): Boolean = {
+    (x / Real(0) == Real(10))
+  }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/RealDivisionByZero.scala b/src/test/resources/regression/verification/purescala/valid/RealDivisionByZero.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3d8dcf5b24e4cf63688ac8d4786be52745e2dd81
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/RealDivisionByZero.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object RealDivisionByZero {
+
+  def noDivByZero(x: Real): Boolean = {
+    (x / Real(10) == Real(10))
+  }
+  
+}