Update overflow tests

test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C  {
+	function f(int x, int y) public pure returns (int) {
+		return x / y;
+	}
+}
+// ----
+// Warning 1218: (110-115): Error trying to invoke SMT solver.
+// Warning 3046: (110-115): Division by zero happens here
+// Warning 2661: (110-115): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here

test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol

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

test/libsolidity/smtCheckerTests/overflow/signed_guard_sum_overflow.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C  {
+	function f(int x, int y) public pure returns (int) {
+		require(x + y >= x);
+		return x + y;
+	}
+}
+// ----
+// Warning 3944: (111-116): Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here
+// Warning 3944: (133-138): Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here

test/libsolidity/smtCheckerTests/overflow/signed_mod_overflow.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C  {
+	function f(int x, int y) public pure returns (int) {
+		return x % y;
+	}
+}
+// ----
+// Warning 3046: (110-115): Division by zero happens here

test/libsolidity/smtCheckerTests/overflow/signed_mul_overflow.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C  {
+	function f(int x, int y) public pure returns (int) {
+		return x * y;
+	}
+}
+// ----
+// Warning 3944: (110-115): Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here
+// Warning 4984: (110-115): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here

test/libsolidity/smtCheckerTests/overflow/signed_sub_overflow.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C  {
+	function f(int x, int y) public pure returns (int) {
+		return x - y;
+	}
+}
+// ----
+// Warning 3944: (110-115): Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here
+// Warning 4984: (110-115): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here

test/libsolidity/smtCheckerTests/overflow/signed_sum_overflow.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C  {
+	function f(int x, int y) public pure returns (int) {
+		return x + y;
+	}
+}
+// ----
+// Warning 3944: (110-115): Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here
+// Warning 4984: (110-115): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here

test/libsolidity/smtCheckerTests/overflow/unsigned_div_overflow.sol

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

test/libsolidity/smtCheckerTests/overflow/unsigned_guard_sub_overflow.sol

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

test/libsolidity/smtCheckerTests/overflow/unsigned_guard_sum_overflow.sol

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

test/libsolidity/smtCheckerTests/overflow/unsigned_mod_overflow.sol

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

test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C  {
+	function f(uint x, uint y) public pure returns (uint) {
+		return x * y;
+	}
+}
+// ----
+// Warning 4984: (113-118): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/overflow/unsigned_sub_overflow.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C  {
+	function f(uint x, uint y) public pure returns (uint) {
+		return x - y;
+	}
+}
+// ----
+// Warning 3944: (113-118): Underflow (resulting value less than 0) happens here

test/libsolidity/smtCheckerTests/overflow/unsigned_sum_overflow.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C  {
+	function f(uint x, uint y) public pure returns (uint) {
+		return x + y;
+	}
+}
+// ----
+// Warning 4984: (113-118): Overflow (resulting value larger than 2**256 - 1) happens here