diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index 8f285c883..549fc05e9 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -218,15 +218,28 @@ SymbolicArrayVariable::SymbolicArrayVariable(
 	solAssert(isArray(m_type->category()), "");
 }
 
+SymbolicArrayVariable::SymbolicArrayVariable(
+	SortPointer _sort,
+	string _uniqueName,
+	EncodingContext& _context
+):
+	SymbolicVariable(move(_sort), move(_uniqueName), _context)
+{
+	solAssert(m_sort->kind == Kind::Array, "");
+}
+
 smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
 {
 	if (_targetType)
+	{
+		solAssert(m_originalType, "");
 		// StringLiterals are encoded as SMT arrays in the generic case,
 		// but they can also be compared/assigned to fixed bytes, in which
 		// case they'd need to be encoded as numbers.
 		if (auto strType = dynamic_cast<StringLiteralType const*>(m_originalType))
 			if (_targetType->category() == frontend::Type::Category::FixedBytes)
 				return smt::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
+	}
 
 	return SymbolicVariable::currentValue(_targetType);
 }
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index be75931f2..e1c28a8b5 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -47,6 +47,8 @@ public:
 		EncodingContext& _context
 	);
 
+	SymbolicVariable(SymbolicVariable&&) = default;
+
 	virtual ~SymbolicVariable() = default;
 
 	virtual Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const;
@@ -212,6 +214,13 @@ public:
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
+	SymbolicArrayVariable(
+		SortPointer _sort,
+		std::string _uniqueName,
+		EncodingContext& _context
+	);
+
+	SymbolicArrayVariable(SymbolicArrayVariable&&) = default;
 
 	Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
 };