diff --git a/Changelog.md b/Changelog.md
index e35ee75a8..9006ac777 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -24,6 +24,7 @@ Bugfixes:
  * NatSpec: DocString block is terminated when encountering an empty line.
  * Scanner: Fix bug when two empty NatSpec comments lead to scanning past EOL.
  * Code Generator: Trigger proper unimplemented errors on certain array copy operations.
+ * SMTChecker: Fix internal error when applying arithmetic operators to fixed point variables.
 
 ### 0.6.8 (2020-05-14)
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 258c74bcc..fd1acb66f 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -463,9 +463,6 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 
 	createExpr(_op);
 
-	if (_op.annotation().type->category() == Type::Category::FixedPoint)
-		return;
-
 	switch (_op.getOperator())
 	{
 	case Token::Not: // !
@@ -477,8 +474,8 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 	case Token::Inc: // ++ (pre- or postfix)
 	case Token::Dec: // -- (pre- or postfix)
 	{
-
-		solAssert(smt::isInteger(_op.annotation().type->category()), "");
+		auto cat = _op.annotation().type->category();
+		solAssert(smt::isInteger(cat) || smt::isFixedPoint(cat), "");
 		solAssert(_op.subExpression().annotation().willBeWrittenTo, "");
 		if (auto identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
 		{
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 0ed81ee31..a46b88e03 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -224,6 +224,8 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 	}
 	else if (isInteger(_type.category()))
 		var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
+	else if (isFixedPoint(_type.category()))
+		var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
 	else if (isFixedBytes(_type.category()))
 	{
 		auto fixedBytesType = dynamic_cast<frontend::FixedBytesType const*>(type);
@@ -272,6 +274,11 @@ bool isInteger(frontend::Type::Category _category)
 	return _category == frontend::Type::Category::Integer;
 }
 
+bool isFixedPoint(frontend::Type::Category _category)
+{
+	return _category == frontend::Type::Category::FixedPoint;
+}
+
 bool isRational(frontend::Type::Category _category)
 {
 	return _category == frontend::Type::Category::RationalNumber;
@@ -300,6 +307,7 @@ bool isEnum(frontend::Type::Category _category)
 bool isNumber(frontend::Type::Category _category)
 {
 	return isInteger(_category) ||
+		isFixedPoint(_category) ||
 		isRational(_category) ||
 		isFixedBytes(_category) ||
 		isAddress(_category) ||
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 2e06f4c86..226bd5f94 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -43,6 +43,7 @@ bool isSupportedTypeDeclaration(frontend::Type::Category _category);
 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);