From 123d0857c57f3f9d87798946b4585312fb461855 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 20 Feb 2019 12:17:03 +0100
Subject: [PATCH] [SMTChecker] Move tests that contain division to boost tests

---
 test/libsolidity/SMTChecker.cpp               | 38 +++++++++++++++++++
 .../smtCheckerTests/overflow/safe_div_1.sol   | 10 -----
 .../smtCheckerTests/overflow/safe_mul_1.sol   | 13 -------
 .../smtCheckerTests/overflow/safe_mul_2.sol   | 15 --------
 4 files changed, 38 insertions(+), 38 deletions(-)
 delete mode 100644 test/libsolidity/smtCheckerTests/overflow/safe_div_1.sol
 delete mode 100644 test/libsolidity/smtCheckerTests/overflow/safe_mul_1.sol
 delete mode 100644 test/libsolidity/smtCheckerTests/overflow/safe_mul_2.sol

diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index a49618bd1..4fd304079 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -94,6 +94,44 @@ BOOST_AUTO_TEST_CASE(division)
 		}
 	)";
 	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function mul(uint256 a, uint256 b) internal pure returns (uint256) {
+				uint256 c;
+				if (a != 0) {
+					c = a * b;
+					require(c / a == b);
+				}
+				return c;
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function mul(uint256 a, uint256 b) internal pure returns (uint256) {
+				if (a == 0) {
+					return 0;
+				}
+				uint256 c = a * b;
+				require(c / a == b);
+				return c;
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Division by zero");
+	text = R"(
+		contract C {
+			function div(uint256 a, uint256 b) internal pure returns (uint256) {
+				require(b > 0);
+				uint256 c = a / b;
+				return c;
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+
+
 }
 
 BOOST_AUTO_TEST_CASE(division_truncates_correctly)
diff --git a/test/libsolidity/smtCheckerTests/overflow/safe_div_1.sol b/test/libsolidity/smtCheckerTests/overflow/safe_div_1.sol
deleted file mode 100644
index 42a0324a4..000000000
--- a/test/libsolidity/smtCheckerTests/overflow/safe_div_1.sol
+++ /dev/null
@@ -1,10 +0,0 @@
-pragma experimental SMTChecker;
-
-contract C
-{
-	function div(uint256 a, uint256 b) internal pure returns (uint256) {
-		require(b > 0);
-		uint256 c = a / b;
-		return c;
-	}
-}
diff --git a/test/libsolidity/smtCheckerTests/overflow/safe_mul_1.sol b/test/libsolidity/smtCheckerTests/overflow/safe_mul_1.sol
deleted file mode 100644
index c93108304..000000000
--- a/test/libsolidity/smtCheckerTests/overflow/safe_mul_1.sol
+++ /dev/null
@@ -1,13 +0,0 @@
-pragma experimental SMTChecker;
-
-contract C
-{
-	function mul(uint256 a, uint256 b) internal pure returns (uint256) {
-		uint256 c;
-		if (a != 0) {
-			c = a * b;
-			require(c / a == b);
-		}
-		return c;
-	}
-}
diff --git a/test/libsolidity/smtCheckerTests/overflow/safe_mul_2.sol b/test/libsolidity/smtCheckerTests/overflow/safe_mul_2.sol
deleted file mode 100644
index b85d368c2..000000000
--- a/test/libsolidity/smtCheckerTests/overflow/safe_mul_2.sol
+++ /dev/null
@@ -1,15 +0,0 @@
-pragma experimental SMTChecker;
-
-contract C
-{
-	function mul(uint256 a, uint256 b) internal pure returns (uint256) {
-		if (a == 0) {
-			return 0;
-		}
-		uint256 c = a * b;
-		require(c / a == b);
-		return c;
-	}
-}
-// ----
-// Warning: (180-185): Division by zero happens here