Merge pull request #6483 from ethereum/smt_support_mod

[SMTChecker] Support mod

test/libsolidity/SMTChecker.cpp

@@ -230,6 +230,22 @@ BOOST_AUTO_TEST_CASE(compound_assignment_division)
 	CHECK_WARNING(text, "Assertion violation");
 }
 
+BOOST_AUTO_TEST_CASE(mod)
+{
+	string text = R"(
+		contract C {
+			function f(int x, int y) public pure {
+				require(y == -10);
+				require(x == 100);
+				int z1 = x % y;
+				int z2 = x % -y;
+				assert(z1 == z2);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }

test/libsolidity/smtCheckerTests/operators/mod_even.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 10000);
+		uint y = x * 2;
+		assert((y % 2) == 0);
+	}
+}

test/libsolidity/smtCheckerTests/operators/mod_n.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, uint y) public pure {
+		require(y > 0);
+		uint z = x % y;
+		assert(z < y);
+	}
+}

test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint16 x, uint16 y) public pure {
+		require(y > 0);
+		uint z = x % y;
+		assert(z < 100_000);
+	}
+}