Extract SMTChecker division tests

test/libsolidity/SMTChecker.cpp

@@ -59,86 +59,6 @@ protected:
 
 BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework)
 
-BOOST_AUTO_TEST_CASE(division)
-{
-	string text = R"(
-		contract C {
-			function f(uint x, uint y) public pure returns (uint) {
-				return x / y;
-			}
-		}
-	)";
-	CHECK_WARNING(text, "Division by zero");
-	text = R"(
-		contract C {
-			function f(uint x, uint y) public pure returns (uint) {
-				require(y != 0);
-				return x / y;
-			}
-		}
-	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
-	text = R"(
-		contract C {
-			function f(int x, int y) public pure returns (int) {
-				require(y != 0);
-				return x / y;
-			}
-		}
-	)";
-	CHECK_WARNING(text, "Overflow");
-	text = R"(
-		contract C {
-			function f(int x, int y) public pure returns (int) {
-				require(y != 0);
-				require(y != -1);
-				return x / y;
-			}
-		}
-	)";
-	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_OR_WARNING(text, "might happen");
-	text = R"(
-		contract C {
-			function mul(uint256 a, uint256 b) internal pure returns (uint256) {
-				if (a == 0) {
-					return 0;
-				}
-				// TODO remove when SMTChecker sees that this code is the `else` of the `return`.
-				require(a != 0);
-				uint256 c = a * b;
-				require(c / a == b);
-				return c;
-			}
-		}
-	)";
-	CHECK_SUCCESS_OR_WARNING(text, "might happen");
-	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)
 {
 	string text = R"(

test/libsolidity/smtCheckerTests/operators/division_1.sol

@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x, uint y) public pure returns (uint) {
+		return x / y;
+	}
+}
+// ----
+// Warning: (111-116): Division by zero happens here

test/libsolidity/smtCheckerTests/operators/division_2.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x, uint y) public pure returns (uint) {
+		require(y != 0);
+		return x / y;
+	}
+}

test/libsolidity/smtCheckerTests/operators/division_3.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(int x, int y) public pure returns (int) {
+		require(y != 0);
+		return x / y;
+	}
+}
+// ----
+// Warning: (127-132): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here

test/libsolidity/smtCheckerTests/operators/division_4.sol

@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(int x, int y) public pure returns (int) {
+		require(y != 0);
+		require(y != -1);
+		return x / y;
+	}
+}

test/libsolidity/smtCheckerTests/operators/division_5.sol

@@ -0,0 +1,11 @@
+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/operators/division_6.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+	function mul(uint256 a, uint256 b) internal pure returns (uint256) {
+		if (a == 0) {
+			return 0;
+		}
+		// TODO remove when SMTChecker sees that this code is the `else` of the `return`.
+		require(a != 0);
+		uint256 c = a * b;
+		require(c / a == b);
+		return c;
+	}
+}

test/libsolidity/smtCheckerTests/operators/division_7.sol

@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+	function div(uint256 a, uint256 b) internal pure returns (uint256) {
+		require(b > 0);
+		uint256 c = a / b;
+		return c;
+	}
+}