Merge pull request #10529 from blishko/compound_assignment

[SMTChecker] Remove assert that is not true for compound assignment with right shift

libsolidity/formal/SMTEncoder.cpp

@@ -1975,12 +1975,6 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
 
 	auto decl = identifierToVariable(_assignment.leftHandSide());
 
-	TypePointer commonType = Type::commonType(
-		_assignment.leftHandSide().annotation().type,
-		_assignment.rightHandSide().annotation().type
-	);
-	solAssert(commonType == _assignment.annotation().type, "");
-
 	if (compoundToBitwise.count(op))
 		return bitwiseOperation(
 			compoundToBitwise.at(op),

test/libsolidity/smtCheckerTests/operators/compound_assignment_right_shift.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(int a, uint b) public view {
+		a >>= tx.gasprice;
+		require(a == 16 && b == 2);
+		a >>= b;
+		assert(a == 4); // should hold
+	}
+}
+// ----