diff --git a/Changelog.md b/Changelog.md
index 2c53509a9..7096c2a40 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -18,6 +18,7 @@ Bugfixes:
  * SMTChecker: Fix false negatives when analyzing external function calls.
  * SMTChecker: Fix missing type constraints for block variables.
  * SMTChecker: Fix internal error on ``block.chainid``.
+ * SMTChecker: Fix internal error on pushing string literal to ``bytes`` array.
  * Type Checker: Fix internal error caused by constant structs containing mappings.
  * Type System: Disallow implicit conversion from ``uintN`` to ``intM`` when ``M > N``, and by extension, explicit conversion between the same types is also disallowed.
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index a2251ab6e..ded438e88 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1547,9 +1547,12 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall)
 	m_context.addAssertion(oldLength + 1 < (smt::maxValue(*TypeProvider::uint256()) - 1));
 
 	auto const& arguments = _funCall.arguments();
+	auto arrayType = dynamic_cast<ArrayType const*>(symbArray->type());
+	solAssert(arrayType, "");
+	auto elementType = arrayType->baseType();
 	smtutil::Expression element = arguments.empty() ?
-		smt::zeroValue(_funCall.annotation().type) :
-		expr(*arguments.front());
+		smt::zeroValue(elementType) :
+		expr(*arguments.front(), elementType);
 	smtutil::Expression store = smtutil::Expression::store(
 		symbArray->elements(),
 		oldLength,
diff --git a/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol b/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol
new file mode 100644
index 000000000..066c73845
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C {
+	bytes data;
+	function g() public {
+		require(data.length == 0);
+		data.push("b");
+		assert(data[0] == "b"); // should hold
+		assert(data[0] == "c"); // should fail
+		delete data;
+		data.push(hex"01");
+		assert(uint8(data[0]) == 1); // should hold
+		assert(uint8(data[0]) == 0); // should fail
+	}
+}
+// ----
+// Warning 6328: (171-193): CHC: Assertion violation happens here.\nCounterexample:\ndata = [98]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()
+// Warning 6328: (295-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = [1]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()