diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 2ff52066d..06c41d732 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/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),
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_right_shift.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_right_shift.sol
new file mode 100644
index 000000000..f49b1ae03
--- /dev/null
+++ b/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
+	}
+}
+// ----