diff --git a/Changelog.md b/Changelog.md
index ae9e14eaa..ae3122813 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -7,8 +7,8 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix internal error on ``FixedBytes`` constant initialized with string literal.
  * SMTChecker: Fix internal error on pushing to ``string`` casted to ``bytes``.
-
 AST Changes:
 
 
diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h
index 4e9cf2258..d880bf7f5 100644
--- a/libsmtutil/SolverInterface.h
+++ b/libsmtutil/SolverInterface.h
@@ -260,6 +260,7 @@ public:
 	}
 	friend Expression operator==(Expression _a, Expression _b)
 	{
+		smtAssert(_a.sort->kind == _b.sort->kind, "Trying to create an 'equal' expression with different sorts");
 		return Expression("=", std::move(_a), std::move(_b), Kind::Bool);
 	}
 	friend Expression operator!=(Expression _a, Expression _b)
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 7aef99856..3afa40160 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -940,7 +940,7 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
 			{
 				solAssert(decl->value(), "");
 				decl->value()->accept(*this);
-				defineExpr(_identifier, expr(*decl->value()));
+				defineExpr(_identifier, expr(*decl->value(), _identifier.annotation().type));
 			}
 		}
 		else
diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_constant_initialization_1.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_constant_initialization_1.sol
new file mode 100644
index 000000000..8763c662d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_constant_initialization_1.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract MockContract {
+	bytes4 public constant SENTINEL_ANY_MOCKS = hex"01";
+	mapping(bytes4 => bytes4) methodIdMocks;
+
+	constructor() {
+		methodIdMocks[SENTINEL_ANY_MOCKS] = 0;
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_constant_initialization_2.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_constant_initialization_2.sol
new file mode 100644
index 000000000..cbef0294f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_constant_initialization_2.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract MockContract {
+	bytes4 public constant SENTINEL_ANY_MOCKS = hex"01";
+
+	constructor() {
+		assert(SENTINEL_ANY_MOCKS >= 0);
+	}
+}