diff --git a/Changelog.md b/Changelog.md
index eb5090c2c..98a1dc275 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -3,6 +3,7 @@
 Compiler Features:
  * SMTChecker: Support ``addmod`` and ``mulmod``.
  * SMTChecker: Support array slices.
+ * SMTChecker: Support type conversions.
  * Optimizer: Optimize ``exp`` when base is -1.
  * Code generator: Implemented events with function type as one of its indexed parameters.
  * General: Option to stop compilation after parsing stage. Can be used with ``solc --stop-after parsing``
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 993f49442..2b42b6c79 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -817,43 +817,125 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
 {
 	solAssert(*_funCall.annotation().kind == FunctionCallKind::TypeConversion, "");
 	solAssert(_funCall.arguments().size() == 1, "");
+
 	auto argument = _funCall.arguments().front();
+	auto const& argType = argument->annotation().type;
+
 	unsigned argSize = argument->annotation().type->storageBytes();
 	unsigned castSize = _funCall.annotation().type->storageBytes();
-	auto const& funCallCategory = _funCall.annotation().type->category();
-	// Allow casting number literals to address.
-	// TODO: remove the isNegative() check once the type checker disallows this
-	if (
-		auto const* numberType = dynamic_cast<RationalNumberType const*>(argument->annotation().type);
-		numberType && !numberType->isNegative() && (funCallCategory == Type::Category::Address)
-	)
-		defineExpr(_funCall, numberType->literalValue(nullptr));
-	else if (argSize == castSize)
-		defineExpr(_funCall, expr(*argument));
-	else
-	{
-		m_context.setUnknownValue(*m_context.expression(_funCall));
-		// TODO: truncating and bytesX needs a different approach because of right padding.
-		if (funCallCategory == Type::Category::Integer || funCallCategory == Type::Category::Address)
-		{
-			if (argSize < castSize)
-				defineExpr(_funCall, expr(*argument));
-			else
-			{
-				auto const& intType = dynamic_cast<IntegerType const&>(*m_context.expression(_funCall)->type());
-				defineExpr(_funCall, smtutil::Expression::ite(
-					expr(*argument) >= smt::minValue(intType) && expr(*argument) <= smt::maxValue(intType),
-					expr(*argument),
-					expr(_funCall)
-				));
-			}
-		}
 
-		m_errorReporter.warning(
-			5084_error,
-			_funCall.location(),
-			"Type conversion is not yet fully supported and might yield false positives."
-		);
+	auto const& funCallType = _funCall.annotation().type;
+
+	// TODO Simplify this whole thing for 0.8.0 where weird casts are disallowed.
+
+	auto symbArg = expr(*argument, funCallType);
+	bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType);
+	bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType);
+	optional<smtutil::Expression> symbMin;
+	optional<smtutil::Expression> symbMax;
+	if (smt::isNumber(*funCallType))
+	{
+		symbMin = smt::minValue(funCallType);
+		symbMax = smt::maxValue(funCallType);
+	}
+	if (argSize == castSize)
+	{
+		// If sizes are the same, it's possible that the signs are different.
+		if (smt::isNumber(*funCallType))
+		{
+			solAssert(smt::isNumber(*argType), "");
+
+			// castIsSigned && !argIsSigned => might overflow if arg > castType.max
+			// !castIsSigned && argIsSigned => might underflow if arg < castType.min
+			// !castIsSigned && !argIsSigned => ok
+			// castIsSigned && argIsSigned => ok
+
+			if (castIsSigned && !argIsSigned)
+			{
+				auto wrap = smtutil::Expression::ite(
+					symbArg > *symbMax,
+					symbArg - (*symbMax - *symbMin + 1),
+					symbArg
+				);
+				defineExpr(_funCall, wrap);
+			}
+			else if (!castIsSigned && argIsSigned)
+			{
+				auto wrap = smtutil::Expression::ite(
+					symbArg < *symbMin,
+					symbArg + (*symbMax + 1),
+					symbArg
+				);
+				defineExpr(_funCall, wrap);
+			}
+			else
+				defineExpr(_funCall, symbArg);
+		}
+		else
+			defineExpr(_funCall, symbArg);
+	}
+	else if (castSize > argSize)
+	{
+		solAssert(smt::isNumber(*funCallType), "");
+		// RationalNumbers have size 32.
+		solAssert(argType->category() != Type::Category::RationalNumber, "");
+
+		// castIsSigned && !argIsSigned => ok
+		// castIsSigned && argIsSigned => ok
+		// !castIsSigned && !argIsSigned => ok except for FixedBytesType, need to adjust padding
+		// !castIsSigned && argIsSigned => might underflow if arg < castType.min
+
+		if (!castIsSigned && argIsSigned)
+		{
+			auto wrap = smtutil::Expression::ite(
+				symbArg < *symbMin,
+				symbArg + (*symbMax + 1),
+				symbArg
+			);
+			defineExpr(_funCall, wrap);
+		}
+		else if (!castIsSigned && !argIsSigned)
+		{
+			if (auto const* fixedCast = dynamic_cast<FixedBytesType const*>(funCallType))
+			{
+				auto const* fixedArg = dynamic_cast<FixedBytesType const*>(argType);
+				solAssert(fixedArg, "");
+				auto diff = fixedCast->numBytes() - fixedArg->numBytes();
+				solAssert(diff > 0, "");
+				auto bvSize = fixedCast->numBytes() * 8;
+				defineExpr(
+					_funCall,
+					smtutil::Expression::bv2int(smtutil::Expression::int2bv(symbArg, bvSize) << smtutil::Expression::int2bv(diff * 8, bvSize))
+				);
+			}
+			else
+				defineExpr(_funCall, symbArg);
+		}
+		else
+			defineExpr(_funCall, symbArg);
+	}
+	else // castSize < argSize
+	{
+		solAssert(smt::isNumber(*funCallType), "");
+
+		auto const* fixedCast = dynamic_cast<FixedBytesType const*>(funCallType);
+		auto const* fixedArg = dynamic_cast<FixedBytesType const*>(argType);
+		if (fixedCast && fixedArg)
+		{
+			createExpr(_funCall);
+			auto diff = argSize - castSize;
+			solAssert(fixedArg->numBytes() - fixedCast->numBytes() == diff, "");
+
+			auto argValueBV = smtutil::Expression::int2bv(symbArg, argSize * 8);
+			auto shr = smtutil::Expression::int2bv(diff * 8, argSize * 8);
+			solAssert(!castIsSigned, "");
+			defineExpr(_funCall, smtutil::Expression::bv2int(argValueBV >> shr));
+		}
+		else
+		{
+			auto argValueBV = smtutil::Expression::int2bv(symbArg, castSize * 8);
+			defineExpr(_funCall, smtutil::Expression::bv2int(argValueBV, castIsSigned));
+		}
 	}
 }
 
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index d363ea0e2..4dcaec474 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -389,11 +389,47 @@ smtutil::Expression minValue(frontend::IntegerType const& _type)
 	return smtutil::Expression(_type.minValue());
 }
 
+smtutil::Expression minValue(frontend::TypePointer _type)
+{
+	solAssert(isNumber(*_type), "");
+	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
+		return intType->minValue();
+	if (auto const* fixedType = dynamic_cast<FixedPointType const*>(_type))
+		return fixedType->minIntegerValue();
+	if (
+		dynamic_cast<AddressType const*>(_type) ||
+		dynamic_cast<ContractType const*>(_type) ||
+		dynamic_cast<EnumType const*>(_type) ||
+		dynamic_cast<FixedBytesType const*>(_type)
+	)
+		return 0;
+	solAssert(false, "");
+}
+
 smtutil::Expression maxValue(frontend::IntegerType const& _type)
 {
 	return smtutil::Expression(_type.maxValue());
 }
 
+smtutil::Expression maxValue(frontend::TypePointer _type)
+{
+	solAssert(isNumber(*_type), "");
+	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
+		return intType->maxValue();
+	if (auto const* fixedType = dynamic_cast<FixedPointType const*>(_type))
+		return fixedType->maxIntegerValue();
+	if (
+		dynamic_cast<AddressType const*>(_type) ||
+		dynamic_cast<ContractType const*>(_type)
+	)
+		return TypeProvider::uint(160)->maxValue();
+	if (auto const* enumType = dynamic_cast<EnumType const*>(_type))
+		return enumType->numberOfMembers();
+	if (auto const* bytesType = dynamic_cast<FixedBytesType const*>(_type))
+		return TypeProvider::uint(bytesType->numBytes() * 8)->maxValue();
+	solAssert(false, "");
+}
+
 void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context)
 {
 	setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _context);
@@ -458,6 +494,29 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type)
 	return 0;
 }
 
+bool isSigned(TypePointer const& _type)
+{
+	solAssert(smt::isNumber(*_type), "");
+	bool isSigned = false;
+	if (auto const* numberType = dynamic_cast<RationalNumberType const*>(_type))
+		isSigned |= numberType->isNegative();
+	else if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
+		isSigned |= intType->isSigned();
+	else if (auto const* fixedType = dynamic_cast<FixedPointType const*>(_type))
+		isSigned |= fixedType->isSigned();
+	else if (
+		dynamic_cast<AddressType const*>(_type) ||
+		dynamic_cast<ContractType const*>(_type) ||
+		dynamic_cast<EnumType const*>(_type) ||
+		dynamic_cast<FixedBytesType const*>(_type)
+	)
+		return false;
+	else
+		solAssert(false, "");
+
+	return isSigned;
+}
+
 pair<unsigned, bool> typeBvSizeAndSignedness(frontend::TypePointer const& _type)
 {
 	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 01bbe4d2c..26a7ad6a4 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -65,8 +65,11 @@ bool isNonRecursiveStruct(frontend::Type const& _type);
 std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(frontend::Type const& _type, std::string const& _uniqueName, EncodingContext& _context);
 
 smtutil::Expression minValue(frontend::IntegerType const& _type);
+smtutil::Expression minValue(frontend::TypePointer _type);
 smtutil::Expression maxValue(frontend::IntegerType const& _type);
+smtutil::Expression maxValue(frontend::TypePointer _type);
 smtutil::Expression zeroValue(frontend::TypePointer const& _type);
+bool isSigned(frontend::TypePointer const& _type);
 
 std::pair<unsigned, bool> typeBvSizeAndSignedness(frontend::TypePointer const& type);
 
diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
index daecc82dc..c29762706 100644
--- a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
+++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
@@ -83,6 +83,5 @@ contract InternalCall {
 // Warning 2018: (1144-1206): Function state mutability can be restricted to pure
 // Warning 2018: (1212-1274): Function state mutability can be restricted to pure
 // Warning 2018: (1280-1342): Function state mutability can be restricted to pure
-// Warning 5084: (782-813): Type conversion is not yet fully supported and might yield false positives.
 // Warning 4588: (771-814): Assertion checker does not yet implement this type of function call.
 // Warning 5729: (1403-1408): Assertion checker does not yet implement this type of function call.
diff --git a/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol b/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol
index 383f907e9..b37bd1a19 100644
--- a/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol
+++ b/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol
@@ -5,4 +5,3 @@ contract C {
     }
 }
 // ----
-// Warning 5084: (106-114): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol
index c3212bb23..b7e16d346 100644
--- a/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol
+++ b/test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol
@@ -5,4 +5,3 @@ contract C {
   }
 }
 // ----
-// Warning 5084: (101-109): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol
index 1431fb248..8682973cd 100644
--- a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol
+++ b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol
@@ -5,4 +5,3 @@ contract C {
   }
 }
 // ----
-// Warning 5084: (102-112): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol
index 4dad0286e..1b937cf9d 100644
--- a/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol
+++ b/test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol
@@ -5,5 +5,3 @@ contract C {
   }
 }
 // ----
-// Warning 5084: (101-111): Type conversion is not yet fully supported and might yield false positives.
-// Warning 5084: (115-125): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol
index 32928e350..9949f930f 100644
--- a/test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol
+++ b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol
@@ -3,10 +3,8 @@ pragma experimental SMTChecker;
 contract C {
 	function f() public pure {
 		uint x = uint(~1);
-		// This assertion fails because type conversion is still unsupported.
 		assert(x == 2**256 - 2);
 		assert(~1 == -2);
 	}
 }
 // ----
-// Warning 6328: (169-192): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol b/test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol
index 7638d3e31..c767d1f32 100644
--- a/test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol
+++ b/test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol
@@ -6,6 +6,3 @@ contract test {
 }
 // ----
 // Warning 2072: (80-88): Unused local variable.
-// Warning 4984: (91-112): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 5084: (91-100): Type conversion is not yet fully supported and might yield false positives.
-// Warning 5084: (103-112): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol b/test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol
index e295f083f..21efadc37 100644
--- a/test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol
@@ -7,20 +7,10 @@ contract C
 		uint32 b = uint16(a); // b will be 0x00001234
 		assert(b == 0x1234);
 		uint32 c = uint32(bytes4(a)); // c will be 0x12340000
-		// This fails because right padding is not supported.
 		assert(c == 0x12340000);
 		uint8 d = uint8(uint16(a)); // d will be 0x34
-		// False positive since truncating is not supported yet.
 		assert(d == 0x34);
 		uint8 e = uint8(bytes1(a)); // e will be 0x12
-		// False positive since truncating is not supported yet.
 		assert(e == 0x12);
 	}
 }
-// ----
-// Warning 6328: (280-303): CHC: Assertion violation happens here.
-// Warning 6328: (414-431): CHC: Assertion violation happens here.
-// Warning 6328: (542-559): CHC: Assertion violation happens here.
-// Warning 5084: (186-195): Type conversion is not yet fully supported and might yield false positives.
-// Warning 5084: (317-333): Type conversion is not yet fully supported and might yield false positives.
-// Warning 5084: (451-460): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol
index af7f1fdf6..6ae5a3378 100644
--- a/test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol
@@ -9,4 +9,3 @@ contract C
 	}
 }
 // ----
-// Warning 5084: (94-103): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol
index 34ef9aef2..bbdeb0bf1 100644
--- a/test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol
@@ -10,4 +10,3 @@ contract C
 	}
 }
 // ----
-// Warning 5084: (108-117): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol
index cfda2b639..738caf10a 100644
--- a/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol
@@ -10,4 +10,3 @@ contract C
 }
 // ----
 // Warning 6328: (149-163): CHC: Assertion violation happens here.
-// Warning 5084: (108-117): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol
index 60879207d..ba109aba2 100644
--- a/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol
@@ -12,6 +12,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (207-230): CHC: Assertion violation happens here.
 // Warning 6328: (273-287): CHC: Assertion violation happens here.
-// Warning 5084: (108-117): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol
index 223141476..310df7e34 100644
--- a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol
@@ -9,4 +9,3 @@ contract C
 	}
 }
 // ----
-// Warning 5084: (94-102): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol
index da8550034..e634cb22a 100644
--- a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol
@@ -5,10 +5,6 @@ contract C
 	function f() public pure {
 		uint32 a = 0x12345678;
 		uint16 b = uint16(a); // b will be 0x5678 now
-		// False positive since truncation is not supported yet.
 		assert(b == 0x5678);
 	}
 }
-// ----
-// Warning 6328: (208-227): CHC: Assertion violation happens here.
-// Warning 5084: (112-121): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol
index 343e80e12..f6d9c36bc 100644
--- a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol
@@ -5,10 +5,6 @@ contract C
 	function f() public pure {
 		bytes2 a = 0x1234;
 		bytes1 b = bytes1(a); // b will be 0x12
-		// False positive since truncation is not supported yet.
 		assert(b == 0x12);
 	}
 }
-// ----
-// Warning 6328: (198-215): CHC: Assertion violation happens here.
-// Warning 5084: (108-117): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/downcast.sol b/test/libsolidity/smtCheckerTests/typecast/downcast.sol
new file mode 100644
index 000000000..53bdbbb7f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/downcast.sol
@@ -0,0 +1,48 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f1() public pure {
+		// signed <- signed
+		int8 z = int8(-1);
+		assert(z == -1);
+		z = int8(0xf0ff);
+		assert(z == -1);
+		z = int8(0xcafecafef0ff);
+		assert(z == -1);
+		z = int8(0xcafecafe);
+		assert(z == -2);
+		z = int8(255);
+		assert(z == -1);
+
+		// unsigned <= unsigned
+		uint8 x = uint8(uint16(-1));
+		assert(x == 255);
+		x = uint8(uint256(-1));
+		assert(x == 255);
+
+		// signed <- unsigned
+		int8 y = int8(uint16(-1));
+		assert(y == -1);
+		y = int8(uint16(100));
+		assert(y == 100);
+		y = int8(uint16(200));
+		assert(y == -56);
+
+		// unsigned <- signed
+		uint8 v = uint8(int16(-1));
+		assert(v == 255);
+		v = uint8(int16(300));
+		assert(v == 44);
+		v = uint8(int16(200));
+		assert(v == 200);
+
+		// fixed bytes
+		bytes2 b = bytes2(bytes4(0xcafeffff));
+		assert(b == 0xcafe);
+		b = bytes2(bytes4(bytes8(0xaaaabbbbccccdddd)));
+		assert(b == 0xaaaa);
+		b = bytes2(bytes8(0xaaaabbbbccccdddd));
+		assert(b == 0xaaaa);
+	}
+}
+// ----
diff --git a/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol b/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol
index ef115ebd2..f14156bde 100644
--- a/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol
@@ -10,6 +10,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (140-160): CHC: Assertion violation happens here.
 // Warning 8364: (132-133): Assertion checker does not yet implement type type(enum C.D)
-// Warning 5084: (132-136): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/enum_to_uint_max_value.sol b/test/libsolidity/smtCheckerTests/typecast/enum_to_uint_max_value.sol
index 419cc6c2d..89b0e7ab0 100644
--- a/test/libsolidity/smtCheckerTests/typecast/enum_to_uint_max_value.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/enum_to_uint_max_value.sol
@@ -9,4 +9,3 @@ contract C
 	}
 }
 // ----
-// Warning 5084: (113-121): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/number_literal.sol b/test/libsolidity/smtCheckerTests/typecast/number_literal.sol
new file mode 100644
index 000000000..b5e99849a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/number_literal.sol
@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract C {
+  function f() public pure {
+    uint x = 1234;
+    uint y = 0;
+    assert(x != y);
+    assert(x == uint(1234));
+    assert(y == uint(0));
+  }
+  function g() public pure {
+    uint a = uint(0);
+    uint b = uint(-1);
+    uint c = 115792089237316195423570985008687907853269984665640564039457584007913129639935;
+    int d = -1;
+    uint e = uint(d);
+    assert(a != b);
+    assert(b == c);
+    assert(b == e);
+  }
+  function h() public pure {
+    uint32 a = uint32(0);
+    uint32 b = uint32(-1);
+    uint32 c = 4294967295;
+    int32 d = -1;
+    uint32 e = uint32(d);
+    assert(a != b);
+    assert(b == c);
+    assert(b == e);
+  }
+}
diff --git a/test/libsolidity/smtCheckerTests/typecast/same_size.sol b/test/libsolidity/smtCheckerTests/typecast/same_size.sol
new file mode 100644
index 000000000..4d5bed1a1
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/same_size.sol
@@ -0,0 +1,74 @@
+pragma experimental SMTChecker;
+
+abstract contract D {}
+
+enum E {A, B}
+
+contract C {
+	function f1() public pure {
+		// signed <- unsigned
+		int8 x = int8(uint8(200));
+		assert(x == -56);
+		int256 y = int256(uint256(2**255 + 10));
+		assert(y == -(2**255) + 10);
+		int256 z = int256(2**255 + 10);
+		assert(z == -(2**255) + 10);
+		int256 t = int256(bytes32(uint256(200)));
+		assert(t == 200);
+		int256 v = int256(bytes32(uint256(2**255 + 10)));
+		assert(v == -(2**255) + 10);
+		int160 a = int160(address(-1));
+		assert(a == -1);
+		int160 b = int160(address(2**159 + 10));
+		assert(b == -(2**159) + 10);
+		D d;
+		int160 e = int160(address(d));
+		assert(e == 0);
+	}
+
+	function f2() public pure {
+		// unsigned <- signed
+		uint8 x = uint8(int8(100));
+		assert(x == 100);
+		uint8 y = uint8(int8(200));
+		assert(y == 200);
+		uint8 z = uint8(int8(-100));
+		assert(z == 156);
+		uint8 t = uint8(int8(-200));
+		assert(t == 56);
+		uint256 v = uint256(int256(-200));
+		assert(v == 2**256 - 200);
+		uint256 w = uint256(-2);
+		assert(w == 2**256 - 2);
+		bytes4 b = bytes4(uint32(-2));
+		assert(uint32(b) == uint32(2**32 - 2));
+		address a = address(-1);
+		assert(uint160(a) == uint160(2**160 - 1));
+		address c = address(0);
+		assert(uint160(c) == 0);
+		D d;
+		address e = address(d);
+		assert(uint160(e) == 0);
+		E f = E(1);
+		assert(uint(f) == 1);
+	}
+
+	function f3() public pure {
+		// unsigned <- unsigned
+		uint8 x = uint8(bytes1(uint8(100)));
+		assert(x == 100);
+		address a = address(0);
+		assert(a == address(uint160(0)));
+		D d;
+		assert(a == address(d));
+	}
+
+	function f4() public pure {
+		// signed <- signed
+		int8 x = -10;
+		int8 y = int8(x);
+		assert(y == -10);
+	}
+}
+// ----
+// Warning 8364: (1304-1305): Assertion checker does not yet implement type type(enum E)
diff --git a/test/libsolidity/smtCheckerTests/typecast/upcast.sol b/test/libsolidity/smtCheckerTests/typecast/upcast.sol
new file mode 100644
index 000000000..8ad35a7d5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/upcast.sol
@@ -0,0 +1,70 @@
+pragma experimental SMTChecker;
+
+abstract contract D {}
+
+contract C {
+	function f1() public pure {
+		// unsigned <- signed
+		uint16 x = uint16(-1);
+		assert(x == 65535);
+		int8 i = int8(-1);
+		assert(i == -1);
+		x = uint16(int8(-1));
+		assert(x == 65535);
+		x = uint16(int16(i));
+		assert(x == 65535);
+		uint z = uint(i);
+		assert(z == 2**256 - 1);
+	}
+
+	function f2() public pure {
+		// signed <- unsigned
+		int16 y = int16(uint8(65535));
+		assert(y == 255);
+		int z = int(uint8(-1));
+		assert(z == 255);
+		z = int(uint8(255));
+		assert(z == 255);
+	}
+
+	function f3() public pure {
+		// signed <- signed
+		int16 y = int16(int8(65535));
+		assert(y == -1);
+		int z = int(int8(-1));
+		assert(z == -1);
+		z = int(int8(255));
+		assert(z == -1);
+		z = int(int16(5000));
+		assert(z == 5000);
+	}
+
+	function f4() public pure {
+		// unsigned <- unsigned
+		uint x = uint(uint8(-1));
+		assert(x == 255);
+		x = uint(uint16(-1));
+		assert(x == 65535);
+		x = uint(uint16(5000));
+		assert(x == 5000);
+		uint16 y = uint16(-1);
+		assert(y == 65535);
+		y = uint16(uint8(-1));
+		assert(y == 255);
+		address a = address(uint8(0));
+		assert(a == address(0));
+		D d = D(uint8(0));
+		assert(a == address(d));
+		bytes2 b1 = 0xcafe;
+		bytes4 b2 = bytes4(b1);
+		assert(b2 == 0xcafe0000);
+		bytes16 b3 = bytes16(b1);
+		assert(b3 == 0xcafe0000000000000000000000000000);
+		bytes4 b4 = bytes4(uint32(0xcafe));
+		assert(b4 == 0x0000cafe);
+		bytes4 b5 = bytes4(uint32(0xcafe0000));
+		assert(b5 == 0xcafe0000);
+	}
+}
+// ----
+// Warning 8364: (1144-1145): Assertion checker does not yet implement type type(contract D)