[SMTChecker] Fix override tests

libsolidity/formal/SMTEncoder.cpp

@@ -52,6 +52,7 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
 			for (auto const& function: resolvedFunctions)
 				if (
 					function->name() == baseFunction->name() &&
+					function->kind() == baseFunction->kind() &&
 					FunctionType(*function).asCallableFunction(false)->
 						hasEqualParameterTypes(*FunctionType(*baseFunction).asCallableFunction(false))
 				)

test/libsolidity/smtCheckerTests/inheritance/fallback.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+// 2 warnings, fallback and A.g
+contract A {
+	uint x;
+
+	fallback () external {
+		assert(x == 1);
+	}
+	function g() public view {
+		assert(x == 1);
+	}
+}
+
+// 2 warnings, fallback and A.g
+contract B is A {
+	uint y;
+
+	fallback () external override {
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (114-128): Assertion violation happens here
+// Warning: (163-177): Assertion violation happens here
+// Warning: (280-294): Assertion violation happens here
+// Warning: (163-177): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+// 2 warnings, fallback and A.g
+contract A {
+	uint x;
+
+	fallback () external {
+		assert(x == 1);
+	}
+	function g() public view {
+		assert(x == 1);
+	}
+}
+
+// 3 warnings, receive, A.fallback and A.g
+contract B is A {
+	uint y;
+
+	receive () external payable {
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (114-128): Assertion violation happens here
+// Warning: (163-177): Assertion violation happens here
+// Warning: (289-303): Assertion violation happens here
+// Warning: (114-128): Assertion violation happens here
+// Warning: (163-177): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/functions_1.sol

@@ -14,12 +14,12 @@ contract A {
 
 // 2 warnings, B.f and A.g
 contract B is A {
-	function f() public view {
+	function f() public view override {
 		assert(x == 0);
 	}
 }
 // ----
 // Warning: (113-127): Assertion violation happens here
 // Warning: (162-176): Assertion violation happens here
-// Warning: (259-273): Assertion violation happens here
+// Warning: (268-282): Assertion violation happens here
 // Warning: (162-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/functions_2.sol

@@ -16,12 +16,12 @@ contract A {
 contract B is A {
 	uint y;
 
-	function f() public view {
+	function f() public view override {
 		assert(x == 0);
 	}
 }
 // ----
 // Warning: (113-127): Assertion violation happens here
 // Warning: (162-176): Assertion violation happens here
-// Warning: (269-283): Assertion violation happens here
+// Warning: (278-292): Assertion violation happens here
 // Warning: (162-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/functions_3.sol

@@ -16,7 +16,7 @@ contract A {
 contract B is A {
 	uint y;
 
-	function f() public view {
+	function f() public view override {
 		assert(x == 0);
 	}
 	function h() public view {
@@ -28,7 +28,7 @@ contract B is A {
 contract C is B {
 	uint z;
 
-	function f() public view {
+	function f() public view override {
 		assert(x == 0);
 	}
 	function i() public view {
@@ -38,10 +38,10 @@ contract C is B {
 // ----
 // Warning: (113-127): Assertion violation happens here
 // Warning: (162-176): Assertion violation happens here
-// Warning: (271-285): Assertion violation happens here
+// Warning: (280-294): Assertion violation happens here
-// Warning: (320-334): Assertion violation happens here
+// Warning: (329-343): Assertion violation happens here
 // Warning: (162-176): Assertion violation happens here
-// Warning: (434-448): Assertion violation happens here
+// Warning: (452-466): Assertion violation happens here
-// Warning: (483-497): Assertion violation happens here
+// Warning: (501-515): Assertion violation happens here
-// Warning: (320-334): Assertion violation happens here
+// Warning: (329-343): Assertion violation happens here
 // Warning: (162-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/receive.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+// 2 warnings, receive and A.g
+contract A {
+	uint x;
+
+	receive () external payable {
+		assert(x == 1);
+	}
+	function g() public view {
+		assert(x == 1);
+	}
+}
+
+// 2 warnings, receive and A.g
+contract B is A {
+	uint y;
+
+	receive () external payable override {
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (120-134): Assertion violation happens here
+// Warning: (169-183): Assertion violation happens here
+// Warning: (292-306): Assertion violation happens here
+// Warning: (169-183): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+// 2 warnings, receive and A.g
+contract A {
+	uint x;
+
+	receive () external payable {
+		assert(x == 1);
+	}
+	function g() public view {
+		assert(x == 1);
+	}
+}
+
+// 3 warnings, fallback, A.receive and A.g
+contract B is A {
+	uint y;
+
+	fallback () external {
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (120-134): Assertion violation happens here
+// Warning: (169-183): Assertion violation happens here
+// Warning: (288-302): Assertion violation happens here
+// Warning: (120-134): Assertion violation happens here
+// Warning: (169-183): Assertion violation happens here