diff --git a/Changelog.md b/Changelog.md
index 047b06ddf..4953a4e49 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -9,6 +9,7 @@ Compiler Features:
  * Yul EVM Code Transform: Free stack slots directly after visiting the right-hand-side of variable declarations instead of at the end of the statement only.
 
 Bugfixes:
+ * SMTChecker: Fix internal error when using bitwise operators on fixed bytes type.
  * Type Checker: Fix overload resolution in combination with ``{value: ...}``.
  * Type Checker: Fix internal compiler error related to oversized types.
 
diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h
index be12c3a80..a62a39b37 100644
--- a/libsmtutil/SolverInterface.h
+++ b/libsmtutil/SolverInterface.h
@@ -59,10 +59,10 @@ class Expression
 public:
 	explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
 	explicit Expression(std::shared_ptr<SortSort> _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {}
-	Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
-	Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
-	Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {}
-	Expression(bigint const& _number): Expression(_number.str(), Kind::Int) {}
+	Expression(size_t _number): Expression(std::to_string(_number), {}, SortProvider::sintSort) {}
+	Expression(u256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
+	Expression(s256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
+	Expression(bigint const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
 
 	Expression(Expression const&) = default;
 	Expression(Expression&&) = default;
@@ -262,23 +262,28 @@ public:
 	}
 	friend Expression operator+(Expression _a, Expression _b)
 	{
-		return Expression("+", std::move(_a), std::move(_b), Kind::Int);
+		auto intSort = _a.sort;
+		return Expression("+", {std::move(_a), std::move(_b)}, intSort);
 	}
 	friend Expression operator-(Expression _a, Expression _b)
 	{
-		return Expression("-", std::move(_a), std::move(_b), Kind::Int);
+		auto intSort = _a.sort;
+		return Expression("-", {std::move(_a), std::move(_b)}, intSort);
 	}
 	friend Expression operator*(Expression _a, Expression _b)
 	{
-		return Expression("*", std::move(_a), std::move(_b), Kind::Int);
+		auto intSort = _a.sort;
+		return Expression("*", {std::move(_a), std::move(_b)}, intSort);
 	}
 	friend Expression operator/(Expression _a, Expression _b)
 	{
-		return Expression("/", std::move(_a), std::move(_b), Kind::Int);
+		auto intSort = _a.sort;
+		return Expression("/", {std::move(_a), std::move(_b)}, intSort);
 	}
 	friend Expression operator%(Expression _a, Expression _b)
 	{
-		return Expression("mod", std::move(_a), std::move(_b), Kind::Int);
+		auto intSort = _a.sort;
+		return Expression("mod", {std::move(_a), std::move(_b)}, intSort);
 	}
 	friend Expression operator&(Expression _a, Expression _b)
 	{
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index eea0b24e5..6a4030511 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1376,9 +1376,11 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
 		bvSize = fixedType->numBits();
 		isSigned = fixedType->isSigned();
 	}
+	else if (auto const* fixedBytesType = dynamic_cast<FixedBytesType const*>(commonType))
+		bvSize = fixedBytesType->numBytes() * 8;
 
-	auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression()), bvSize);
-	auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression()), bvSize);
+	auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression(), commonType), bvSize);
+	auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression(), commonType), bvSize);
 
 	optional<smtutil::Expression> result;
 	if (_op.getOperator() == Token::BitAnd)
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index a46b88e03..096f496c4 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -441,7 +441,11 @@ optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePoin
 		// case they'd need to be encoded as numbers.
 		if (auto strType = dynamic_cast<StringLiteralType const*>(_from))
 			if (_to->category() == frontend::Type::Category::FixedBytes)
+			{
+				if (strType->value().empty())
+					return smtutil::Expression(size_t(0));
 				return smtutil::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
+			}
 
 	return std::nullopt;
 }
diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol
new file mode 100644
index 000000000..c3212bb23
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+  function f() public pure returns (byte) {
+    return (byte("") & (""));
+  }
+}
+// ----
+// Warning 5084: (101-109): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol
new file mode 100644
index 000000000..3852563be
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract Simp {
+    function f3() public pure returns (byte) {
+        bytes memory y = "def";
+        return y[0] ^ "e";
+    }
+}
+// ----
+// Warning 1093: (142-152): Assertion checker does not yet implement this bitwise operator.