From e233402c7a9e96ac84e0089eeec8d45f1f90687b Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 8 May 2015 14:22:08 +0200
Subject: [PATCH] testing bv division by zero with variables
---
.../verification/purescala/invalid/BVDivision2.scala | 11 +++++++++++
.../verification/purescala/valid/BVDivision2.scala | 12 ++++++++++++
2 files changed, 23 insertions(+)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/BVDivision2.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/BVDivision2.scala
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 000000000..c11405429
--- /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 000000000..77d677753
--- /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
+ }
+
+}
--
GitLab