diff --git a/Changelog.md b/Changelog.md
index 07ab24363..50a3e4d1e 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -7,6 +7,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix internal error when fixed points are used.
  * Type Checker: Disallow ``virtual`` and ``override`` for constructors.
  * Type Checker: Fix several internal errors by performing size and recursiveness checks of types before the full type checking.
  * Type Checker: Perform recursiveness check on structs declared at the file level.
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 1b4e8174a..13a19694b 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -304,7 +304,10 @@ void BMC::endVisit(UnaryOperation const& _op)
 {
 	SMTEncoder::endVisit(_op);
 
-	if (_op.annotation().type->category() == Type::Category::RationalNumber)
+	if (
+		_op.annotation().type->category() == Type::Category::RationalNumber ||
+		_op.annotation().type->category() == Type::Category::FixedPoint
+	)
 		return;
 
 	switch (_op.getOperator())
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 820af022e..12c9971dc 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -457,6 +457,9 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 
 	createExpr(_op);
 
+	if (_op.annotation().type->category() == Type::Category::FixedPoint)
+		return;
+
 	switch (_op.getOperator())
 	{
 	case Token::Not: // !