[SMTChecker] added test to check correct handling of the sign of the modulo operation

test/libsolidity/smtCheckerTests/operators/mod_signed.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(int x, int y) public pure {
+		require(y != 0);
+		require(x == 42);
+		int z1 = x % y;
+		int z2 = -x % y;
+		assert(z1 == -z2);
+		assert((x >= 0 && z1 >=0) || (x <= 0 && z1 <= 0));
+	}
+}
+// ----