check for division by zero of real numbers

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
       }) 

src/test/resources/regression/verification/purescala/invalid/RealDivisionByZero.scala

+import leon.lang._
+import leon.collection._
+import leon._
+
+object RealDivisionByZero {
+
+  def divByZero(x: Real): Boolean = {
+    (x / Real(0) == Real(10))
+  }
+
+}

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

+import leon.lang._
+import leon.collection._
+import leon._
+
+object RealDivisionByZero {
+
+  def noDivByZero(x: Real): Boolean = {
+    (x / Real(10) == Real(10))
+  }
+  
+}