diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 503f48da8..a47ca647f 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -580,7 +580,7 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
 		auto const& type = var.second->type();
 		if (
 			type->isValueType() &&
-			smt::smtKind(type->category()) != smtutil::Kind::Function
+			smt::smtKind(*type) != smtutil::Kind::Function
 		)
 		{
 			expressionsToEvaluate.emplace_back(var.second->currentValue());
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 057d67daa..b8e5ac791 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -378,7 +378,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 			"Assertion checker does not yet implement this assignment operator."
 		);
 	}
-	else if (!smt::isSupportedType(_assignment.annotation().type->category()))
+	else if (!smt::isSupportedType(*_assignment.annotation().type))
 	{
 		// Give it a new index anyway to keep the SSA scheme sound.
 
@@ -462,20 +462,19 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 	createExpr(_op);
 
 	auto const* subExpr = innermostTuple(_op.subExpression());
-
+	auto type = _op.annotation().type;
 	switch (_op.getOperator())
 	{
 	case Token::Not: // !
 	{
-		solAssert(smt::isBool(_op.annotation().type->category()), "");
+		solAssert(smt::isBool(*type), "");
 		defineExpr(_op, !expr(*subExpr));
 		break;
 	}
 	case Token::Inc: // ++ (pre- or postfix)
 	case Token::Dec: // -- (pre- or postfix)
 	{
-		auto cat = _op.annotation().type->category();
-		solAssert(smt::isInteger(cat) || smt::isFixedPoint(cat), "");
+		solAssert(smt::isInteger(*type) || smt::isFixedPoint(*type), "");
 		solAssert(subExpr->annotation().willBeWrittenTo, "");
 		if (auto identifier = dynamic_cast<Identifier const*>(subExpr))
 		{
@@ -486,7 +485,10 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 			defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
 			assignment(*decl, newValue);
 		}
-		else if (dynamic_cast<IndexAccess const*>(subExpr))
+		else if (
+			dynamic_cast<IndexAccess const*>(&_op.subExpression()) ||
+			dynamic_cast<MemberAccess const*>(&_op.subExpression())
+		)
 		{
 			auto innerValue = expr(*subExpr);
 			auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
@@ -824,11 +826,11 @@ void SMTEncoder::endVisit(Literal const& _literal)
 {
 	solAssert(_literal.annotation().type, "Expected type for AST node");
 	Type const& type = *_literal.annotation().type;
-	if (smt::isNumber(type.category()))
+	if (smt::isNumber(type))
 		defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal)));
-	else if (smt::isBool(type.category()))
+	else if (smt::isBool(type))
 		defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));
-	else if (smt::isStringLiteral(type.category()))
+	else if (smt::isStringLiteral(type))
 		createExpr(_literal);
 	else
 	{
@@ -891,7 +893,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 		defineGlobalVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
 		return false;
 	}
-	else if (exprType->category() == Type::Category::Struct)
+	else if (smt::isNonRecursiveStruct(*exprType))
 	{
 		_memberAccess.expression().accept(*this);
 		auto const& symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(_memberAccess.expression()));
@@ -1034,6 +1036,20 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
 			auto const& base = memberAccess->expression();
 			if (dynamic_cast<Identifier const*>(&base))
 				base.accept(*this);
+
+			if (
+				auto const* structType = dynamic_cast<StructType const*>(base.annotation().type);
+				structType && structType->recursive()
+			)
+			{
+				m_errorReporter.warning(
+					4375_error,
+					memberAccess->location(),
+					"Assertion checker does not support recursive structs."
+				);
+				return;
+			}
+
 			auto symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(base));
 			solAssert(symbStruct, "");
 			symbStruct->assignMember(memberAccess->memberName(), toStore);
@@ -1186,7 +1202,7 @@ void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _ex
 		m_context.globalSymbol(_name)->increaseIndex();
 	// The default behavior is not to increase the index since
 	// most of the global values stay the same throughout a tx.
-	if (smt::isSupportedType(_expr.annotation().type->category()))
+	if (smt::isSupportedType(*_expr.annotation().type))
 		defineExpr(_expr, m_context.globalSymbol(_name)->currentValue());
 }
 
@@ -1339,13 +1355,13 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
 {
 	auto const& commonType = _op.annotation().commonType;
 	solAssert(commonType, "");
-	if (smt::isSupportedType(commonType->category()))
+	if (smt::isSupportedType(*commonType))
 	{
 		smtutil::Expression left(expr(_op.leftExpression(), commonType));
 		smtutil::Expression right(expr(_op.rightExpression(), commonType));
 		Token op = _op.getOperator();
 		shared_ptr<smtutil::Expression> value;
-		if (smt::isNumber(commonType->category()))
+		if (smt::isNumber(*commonType))
 		{
 			value = make_shared<smtutil::Expression>(
 				op == Token::Equal ? (left == right) :
@@ -1358,7 +1374,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
 		}
 		else // Bool
 		{
-			solUnimplementedAssert(smt::isBool(commonType->category()), "Operation not yet supported");
+			solUnimplementedAssert(smt::isBool(*commonType), "Operation not yet supported");
 			value = make_shared<smtutil::Expression>(
 				op == Token::Equal ? (left == right) :
 				/*op == Token::NotEqual*/ (left != right)
@@ -1464,7 +1480,7 @@ void SMTEncoder::assignment(
 
 	Expression const* left = innermostTuple(_left);
 
-	if (!smt::isSupportedType(_type->category()))
+	if (!smt::isSupportedType(*_type))
 	{
 		// Give it a new index anyway to keep the SSA scheme sound.
 		if (auto varDecl = identifierToVariable(*left))
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 1d4f2fb82..d363ea0e2 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -33,7 +33,7 @@ namespace solidity::frontend::smt
 
 SortPointer smtSort(frontend::Type const& _type)
 {
-	switch (smtKind(_type.category()))
+	switch (smtKind(_type))
 	{
 	case Kind::Int:
 		if (auto const* intType = dynamic_cast<IntegerType const*>(&_type))
@@ -64,13 +64,13 @@ SortPointer smtSort(frontend::Type const& _type)
 	case Kind::Array:
 	{
 		shared_ptr<ArraySort> array;
-		if (isMapping(_type.category()))
+		if (isMapping(_type))
 		{
 			auto mapType = dynamic_cast<frontend::MappingType const*>(&_type);
 			solAssert(mapType, "");
 			array = make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
 		}
-		else if (isStringLiteral(_type.category()))
+		else if (isStringLiteral(_type))
 		{
 			auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type);
 			solAssert(stringLitType, "");
@@ -144,6 +144,7 @@ SortPointer smtSort(frontend::Type const& _type)
 		}
 		else if (auto const* structType = dynamic_cast<frontend::StructType const*>(&_type))
 		{
+			solAssert(!structType->recursive(), "");
 			auto const& structMembers = structType->structDefinition().members();
 			for (auto member: structMembers)
 				members.emplace_back(tupleName + "_accessor_" + member->name());
@@ -173,7 +174,7 @@ vector<SortPointer> smtSort(vector<frontend::TypePointer> const& _types)
 
 SortPointer smtSortAbstractFunction(frontend::Type const& _type)
 {
-	if (isFunction(_type.category()))
+	if (isFunction(_type))
 		return SortProvider::uintSort;
 	return smtSort(_type);
 }
@@ -189,36 +190,36 @@ vector<SortPointer> smtSortAbstractFunction(vector<frontend::TypePointer> const&
 	return sorts;
 }
 
-Kind smtKind(frontend::Type::Category _category)
+Kind smtKind(frontend::Type const& _type)
 {
-	if (isNumber(_category))
+	if (isNumber(_type))
 		return Kind::Int;
-	else if (isBool(_category))
+	else if (isBool(_type))
 		return Kind::Bool;
-	else if (isFunction(_category))
+	else if (isFunction(_type))
 		return Kind::Function;
-	else if (isMapping(_category) || isArray(_category))
+	else if (isMapping(_type) || isArray(_type))
 		return Kind::Array;
-	else if (isTuple(_category) || isStruct(_category))
+	else if (isTuple(_type) || isNonRecursiveStruct(_type))
 		return Kind::Tuple;
 	// Abstract case.
 	return Kind::Int;
 }
 
-bool isSupportedType(frontend::Type::Category _category)
+bool isSupportedType(frontend::Type const& _type)
 {
-	return isNumber(_category) ||
-		isBool(_category) ||
-		isMapping(_category) ||
-		isArray(_category) ||
-		isTuple(_category) ||
-		isStruct(_category);
+	return isNumber(_type) ||
+		isBool(_type) ||
+		isMapping(_type) ||
+		isArray(_type) ||
+		isTuple(_type) ||
+		isNonRecursiveStruct(_type);
 }
 
-bool isSupportedTypeDeclaration(frontend::Type::Category _category)
+bool isSupportedTypeDeclaration(frontend::Type const& _type)
 {
-	return isSupportedType(_category) ||
-		isFunction(_category);
+	return isSupportedType(_type) ||
+		isFunction(_type);
 }
 
 pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
@@ -235,9 +236,9 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		abstract = true;
 		var = make_shared<SymbolicIntVariable>(frontend::TypeProvider::uint256(), type, _uniqueName, _context);
 	}
-	else if (isBool(_type.category()))
+	else if (isBool(_type))
 		var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _context);
-	else if (isFunction(_type.category()))
+	else if (isFunction(_type))
 	{
 		auto const& fType = dynamic_cast<FunctionType const*>(type);
 		auto const& paramsIn = fType->parameterTypes();
@@ -260,21 +261,21 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		else
 			var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
 	}
-	else if (isInteger(_type.category()))
+	else if (isInteger(_type))
 		var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
-	else if (isFixedPoint(_type.category()))
+	else if (isFixedPoint(_type))
 		var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
-	else if (isFixedBytes(_type.category()))
+	else if (isFixedBytes(_type))
 	{
 		auto fixedBytesType = dynamic_cast<frontend::FixedBytesType const*>(type);
 		solAssert(fixedBytesType, "");
 		var = make_shared<SymbolicFixedBytesVariable>(type, fixedBytesType->numBytes(), _uniqueName, _context);
 	}
-	else if (isAddress(_type.category()) || isContract(_type.category()))
+	else if (isAddress(_type) || isContract(_type))
 		var = make_shared<SymbolicAddressVariable>(_uniqueName, _context);
-	else if (isEnum(_type.category()))
+	else if (isEnum(_type))
 		var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _context);
-	else if (isRational(_type.category()))
+	else if (isRational(_type))
 	{
 		auto rational = dynamic_cast<frontend::RationalNumberType const*>(&_type);
 		solAssert(rational, "");
@@ -283,113 +284,104 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		else
 			var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
 	}
-	else if (isMapping(_type.category()) || isArray(_type.category()))
+	else if (isMapping(_type) || isArray(_type))
 		var = make_shared<SymbolicArrayVariable>(type, type, _uniqueName, _context);
-	else if (isTuple(_type.category()))
+	else if (isTuple(_type))
 		var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _context);
-	else if (isStringLiteral(_type.category()))
+	else if (isStringLiteral(_type))
 	{
 		auto stringType = TypeProvider::stringMemory();
 		var = make_shared<SymbolicArrayVariable>(stringType, type, _uniqueName, _context);
 	}
-	else if (isStruct(_type.category()))
+	else if (isNonRecursiveStruct(_type))
 		var = make_shared<SymbolicStructVariable>(type, _uniqueName, _context);
 	else
 		solAssert(false, "");
 	return make_pair(abstract, var);
 }
 
-bool isSupportedType(frontend::Type const& _type)
+bool isInteger(frontend::Type const& _type)
 {
-	return isSupportedType(_type.category());
+	return _type.category() == frontend::Type::Category::Integer;
 }
 
-bool isSupportedTypeDeclaration(frontend::Type const& _type)
+bool isFixedPoint(frontend::Type const& _type)
 {
-	return isSupportedTypeDeclaration(_type.category());
+	return _type.category() == frontend::Type::Category::FixedPoint;
 }
 
-bool isInteger(frontend::Type::Category _category)
+bool isRational(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Integer;
+	return _type.category() == frontend::Type::Category::RationalNumber;
 }
 
-bool isFixedPoint(frontend::Type::Category _category)
+bool isFixedBytes(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::FixedPoint;
+	return _type.category() == frontend::Type::Category::FixedBytes;
 }
 
-bool isRational(frontend::Type::Category _category)
+bool isAddress(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::RationalNumber;
+	return _type.category() == frontend::Type::Category::Address;
 }
 
-bool isFixedBytes(frontend::Type::Category _category)
+bool isContract(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::FixedBytes;
+	return _type.category() == frontend::Type::Category::Contract;
 }
 
-bool isAddress(frontend::Type::Category _category)
+bool isEnum(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Address;
+	return _type.category() == frontend::Type::Category::Enum;
 }
 
-bool isContract(frontend::Type::Category _category)
+bool isNumber(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Contract;
+	return isInteger(_type) ||
+		isFixedPoint(_type) ||
+		isRational(_type) ||
+		isFixedBytes(_type) ||
+		isAddress(_type) ||
+		isContract(_type) ||
+		isEnum(_type);
 }
 
-bool isEnum(frontend::Type::Category _category)
+bool isBool(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Enum;
+	return _type.category() == frontend::Type::Category::Bool;
 }
 
-bool isNumber(frontend::Type::Category _category)
+bool isFunction(frontend::Type const& _type)
 {
-	return isInteger(_category) ||
-		isFixedPoint(_category) ||
-		isRational(_category) ||
-		isFixedBytes(_category) ||
-		isAddress(_category) ||
-		isContract(_category) ||
-		isEnum(_category);
+	return _type.category() == frontend::Type::Category::Function;
 }
 
-bool isBool(frontend::Type::Category _category)
+bool isMapping(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Bool;
+	return _type.category() == frontend::Type::Category::Mapping;
 }
 
-bool isFunction(frontend::Type::Category _category)
+bool isArray(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Function;
+	return _type.category() == frontend::Type::Category::Array ||
+		_type.category() == frontend::Type::Category::StringLiteral ||
+		_type.category() == frontend::Type::Category::ArraySlice;
 }
 
-bool isMapping(frontend::Type::Category _category)
+bool isTuple(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Mapping;
+	return _type.category() == frontend::Type::Category::Tuple;
 }
 
-bool isArray(frontend::Type::Category _category)
+bool isStringLiteral(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Array ||
-		_category == frontend::Type::Category::StringLiteral ||
-		_category == frontend::Type::Category::ArraySlice;
+	return _type.category() == frontend::Type::Category::StringLiteral;
 }
 
-bool isTuple(frontend::Type::Category _category)
+bool isNonRecursiveStruct(frontend::Type const& _type)
 {
-	return _category == frontend::Type::Category::Tuple;
-}
-
-bool isStringLiteral(frontend::Type::Category _category)
-{
-	return _category == frontend::Type::Category::StringLiteral;
-}
-
-bool isStruct(frontend::Type::Category _category)
-{
-	return _category == frontend::Type::Category::Struct;
+	auto structType = dynamic_cast<StructType const*>(&_type);
+	return structType && !structType->recursive();
 }
 
 smtutil::Expression minValue(frontend::IntegerType const& _type)
@@ -416,13 +408,13 @@ void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const
 smtutil::Expression zeroValue(frontend::TypePointer const& _type)
 {
 	solAssert(_type, "");
-	if (isSupportedType(_type->category()))
+	if (isSupportedType(*_type))
 	{
-		if (isNumber(_type->category()))
+		if (isNumber(*_type))
 			return 0;
-		if (isBool(_type->category()))
+		if (isBool(*_type))
 			return smtutil::Expression(false);
-		if (isArray(_type->category()) || isMapping(_type->category()))
+		if (isArray(*_type) || isMapping(*_type))
 		{
 			auto tupleSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
 			solAssert(tupleSort, "");
@@ -448,10 +440,9 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type)
 			);
 
 		}
-		if (isStruct(_type->category()))
+		if (isNonRecursiveStruct(*_type))
 		{
 			auto const* structType = dynamic_cast<StructType const*>(_type);
-			solAssert(structType, "");
 			auto structSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
 			return smtutil::Expression::tuple_constructor(
 				smtutil::Expression(make_shared<SortSort>(structSort), structSort->name),
@@ -487,14 +478,14 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext&
 void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
 {
 	solAssert(_type, "");
-	if (isEnum(_type->category()))
+	if (isEnum(*_type))
 	{
 		auto enumType = dynamic_cast<frontend::EnumType const*>(_type);
 		solAssert(enumType, "");
 		_context.addAssertion(_expr >= 0);
 		_context.addAssertion(_expr < enumType->numberOfMembers());
 	}
-	else if (isInteger(_type->category()))
+	else if (isInteger(*_type))
 	{
 		auto intType = dynamic_cast<frontend::IntegerType const*>(_type);
 		solAssert(intType, "");
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 1c38645d9..01bbe4d2c 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -34,30 +34,30 @@ std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::TypePointer> con
 smtutil::SortPointer smtSortAbstractFunction(frontend::Type const& _type);
 std::vector<smtutil::SortPointer> smtSortAbstractFunction(std::vector<frontend::TypePointer> const& _types);
 /// Returns the SMT kind that models the Solidity type type category _category.
-smtutil::Kind smtKind(frontend::Type::Category _category);
+smtutil::Kind smtKind(frontend::Type const& _type);
 
 /// Returns true if type is fully supported (declaration and operations).
-bool isSupportedType(frontend::Type::Category _category);
+bool isSupportedType(frontend::Type const& _type);
 bool isSupportedType(frontend::Type const& _type);
 /// Returns true if type is partially supported (declaration).
-bool isSupportedTypeDeclaration(frontend::Type::Category _category);
+bool isSupportedTypeDeclaration(frontend::Type const& _type);
 bool isSupportedTypeDeclaration(frontend::Type const& _type);
 
-bool isInteger(frontend::Type::Category _category);
-bool isFixedPoint(frontend::Type::Category _category);
-bool isRational(frontend::Type::Category _category);
-bool isFixedBytes(frontend::Type::Category _category);
-bool isAddress(frontend::Type::Category _category);
-bool isContract(frontend::Type::Category _category);
-bool isEnum(frontend::Type::Category _category);
-bool isNumber(frontend::Type::Category _category);
-bool isBool(frontend::Type::Category _category);
-bool isFunction(frontend::Type::Category _category);
-bool isMapping(frontend::Type::Category _category);
-bool isArray(frontend::Type::Category _category);
-bool isTuple(frontend::Type::Category _category);
-bool isStringLiteral(frontend::Type::Category _category);
-bool isStruct(frontend::Type::Category _category);
+bool isInteger(frontend::Type const& _type);
+bool isFixedPoint(frontend::Type const& _type);
+bool isRational(frontend::Type const& _type);
+bool isFixedBytes(frontend::Type const& _type);
+bool isAddress(frontend::Type const& _type);
+bool isContract(frontend::Type const& _type);
+bool isEnum(frontend::Type const& _type);
+bool isNumber(frontend::Type const& _type);
+bool isBool(frontend::Type const& _type);
+bool isFunction(frontend::Type const& _type);
+bool isMapping(frontend::Type const& _type);
+bool isArray(frontend::Type const& _type);
+bool isTuple(frontend::Type const& _type);
+bool isStringLiteral(frontend::Type const& _type);
+bool isNonRecursiveStruct(frontend::Type const& _type);
 
 /// Returns a new symbolic variable, according to _type.
 /// Also returns whether the type is abstract or not,
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index e0852d4d7..51711b383 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -121,7 +121,7 @@ SymbolicIntVariable::SymbolicIntVariable(
 ):
 	SymbolicVariable(_type, _originalType, move(_uniqueName), _context)
 {
-	solAssert(isNumber(m_type->category()), "");
+	solAssert(isNumber(*m_type), "");
 }
 
 SymbolicAddressVariable::SymbolicAddressVariable(
@@ -221,7 +221,7 @@ SymbolicEnumVariable::SymbolicEnumVariable(
 ):
 	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
-	solAssert(isEnum(m_type->category()), "");
+	solAssert(isEnum(*m_type), "");
 }
 
 SymbolicTupleVariable::SymbolicTupleVariable(
@@ -231,7 +231,7 @@ SymbolicTupleVariable::SymbolicTupleVariable(
 ):
 	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
-	solAssert(isTuple(m_type->category()), "");
+	solAssert(isTuple(*m_type), "");
 }
 
 SymbolicTupleVariable::SymbolicTupleVariable(
@@ -277,7 +277,7 @@ SymbolicArrayVariable::SymbolicArrayVariable(
 		m_context
 	)
 {
-	solAssert(isArray(m_type->category()) || isMapping(m_type->category()), "");
+	solAssert(isArray(*m_type) || isMapping(*m_type), "");
 }
 
 SymbolicArrayVariable::SymbolicArrayVariable(
@@ -330,7 +330,7 @@ SymbolicStructVariable::SymbolicStructVariable(
 ):
 	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
-	solAssert(isStruct(m_type->category()), "");
+	solAssert(isNonRecursiveStruct(*m_type), "");
 	auto const* structType = dynamic_cast<StructType const*>(_type);
 	solAssert(structType, "");
 	auto const& members = structType->structDefinition().members();