Merge pull request #6046 from ethereum/smt_division_tests

[SMTChecker] Move tests that contain division to boost tests

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)

test/libsolidity/smtCheckerTests/overflow/safe_div_1.sol

@@ -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;
-	}
-}

test/libsolidity/smtCheckerTests/overflow/safe_mul_1.sol

@@ -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;
-	}
-}

test/libsolidity/smtCheckerTests/overflow/safe_mul_2.sol

@@ -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