Merge pull request #10127 from ethereum/fixIceSmtBitwise

[SMTChecker] Fix ICE when using >>>

libsolidity/formal/SMTEncoder.cpp

@@ -1653,7 +1653,8 @@ smtutil::Expression SMTEncoder::bitwiseOperation(
 			result = bvLeft << bvRight;
 			break;
 		case Token::SHR:
-			solAssert(false, "");
+			result = bvLeft >> bvRight;
+			break;
 		case Token::SAR:
 			result = isSigned ?
 				smtutil::Expression::ashr(bvLeft, bvRight) :

test/libsolidity/smtCheckerTests/operators/shifts/shr_unused.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		fixed x;
+		assert(x >>> 6 == 0);
+	}
+}
+// ----
+// UnimplementedFeatureError: Not yet implemented - FixedPointType.