diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 8ec6b3564..8f74dbb3e 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -604,7 +604,11 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression con
 			_target.type == VerificationTarget::Type::UnderOverflow,
 		""
 	);
-	auto intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
+	IntegerType const* intType = nullptr;
+	if (auto const* type = dynamic_cast<IntegerType const*>(_target.expression->annotation().type))
+		intType = type;
+	else
+		intType = TypeProvider::uint256();
 	solAssert(intType, "");
 	checkCondition(
 		_target.constraints && _constraints && _target.value < smt::minValue(*intType),
@@ -626,7 +630,12 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression cons
 			_target.type == VerificationTarget::Type::UnderOverflow,
 		""
 	);
-	auto intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
+	IntegerType const* intType = nullptr;
+	if (auto const* type = dynamic_cast<IntegerType const*>(_target.expression->annotation().type))
+		intType = type;
+	else
+		intType = TypeProvider::uint256();
+
 	solAssert(intType, "");
 	checkCondition(
 		_target.constraints && _constraints && _target.value > smt::maxValue(*intType),
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index b06abbe6e..01520f503 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1213,7 +1213,7 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
 {
 	auto type = _op.annotation().commonType;
 	solAssert(type, "");
-	if (type->category() == Type::Category::Integer)
+	if (type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint)
 	{
 		switch (_op.getOperator())
 		{
@@ -1266,13 +1266,21 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 	};
 	solAssert(validOperators.count(_op), "");
 	solAssert(_commonType, "");
-	solAssert(_commonType->category() == Type::Category::Integer, "");
+	solAssert(
+		_commonType->category() == Type::Category::Integer || _commonType->category() == Type::Category::FixedPoint,
+		""
+	);
+
+	IntegerType const* intType = nullptr;
+	if (auto type = dynamic_cast<IntegerType const*>(_commonType))
+		intType = type;
+	else
+		intType = TypeProvider::uint256();
 
-	auto const& intType = dynamic_cast<IntegerType const&>(*_commonType);
 	smtutil::Expression valueNoMod(
 		_op == Token::Add ? _left + _right :
 		_op == Token::Sub ? _left - _right :
-		_op == Token::Div ? division(_left, _right, intType) :
+		_op == Token::Div ? division(_left, _right, *intType) :
 		_op == Token::Mul ? _left * _right :
 		/*_op == Token::Mod*/ _left % _right
 	);
@@ -1280,20 +1288,23 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 	if (_op == Token::Div || _op == Token::Mod)
 		m_context.addAssertion(_right != 0);
 
-	smtutil::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1;
+	auto symbMin = smt::minValue(*intType);
+	auto symbMax = smt::maxValue(*intType);
+
+	smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1;
 	auto value = smtutil::Expression::ite(
-		valueNoMod > smt::maxValue(intType),
+		valueNoMod > symbMax,
 		valueNoMod % intValueRange,
 		smtutil::Expression::ite(
-			valueNoMod < smt::minValue(intType),
+			valueNoMod < symbMin,
 			valueNoMod % intValueRange,
 			valueNoMod
 		)
 	);
 
-	if (intType.isSigned())
+	if (intType->isSigned())
 		value = smtutil::Expression::ite(
-			value > smt::maxValue(intType),
+			value > symbMax,
 			value - intValueRange,
 			value
 		);
diff --git a/test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol b/test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol
new file mode 100644
index 000000000..23a05e619
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract test {
+	function f() internal pure {
+		ufixed a = uint64(1) + ufixed(2);
+	}
+}
+// ----
+// Warning: (80-88): Unused local variable.
+// Warning: (91-100): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (103-112): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (91-112): Underflow (resulting value less than 0) happens here
+// Warning: (91-112): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/fixed_point_compound_add.sol b/test/libsolidity/smtCheckerTests/operators/fixed_point_compound_add.sol
new file mode 100644
index 000000000..d4cbbc696
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/fixed_point_compound_add.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+  fixed[] b;
+  function f() internal { b[0] += 1; }
+}
+// ----
+// Warning: (84-93): Underflow (resulting value less than 0) happens here
+// Warning: (84-93): Overflow (resulting value larger than 2**256 - 1) happens here