generate vc for division by zero

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
               }

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

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]) {

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

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

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

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

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

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

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

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