diff --git a/src/test/resources/regression/verification/purescala/invalid/BVDivision2.scala b/src/test/resources/regression/verification/purescala/invalid/BVDivision2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c11405429d270758774cf20ef5f8be650a375937
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/BVDivision2.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object BVDivision2 {
+
+  def division(x: Int, y: Int): Int = {
+    x / y
+  }
+  
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/BVDivision2.scala b/src/test/resources/regression/verification/purescala/valid/BVDivision2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..77d677753e0c8aed018625f14d3d3b6d0a5ee0e8
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/BVDivision2.scala
@@ -0,0 +1,12 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object BVDivision2 {
+
+  def division(x: Int, y: Int): Int = {
+    require(y != 0)
+    x / y
+  }
+  
+}