diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp
index e4ea16545..5d605f732 100644
--- a/libsmtutil/SMTLib2Interface.cpp
+++ b/libsmtutil/SMTLib2Interface.cpp
@@ -244,6 +244,8 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 
 		return tupleName;
 	}
+	case Kind::Real:
+		return "Real";
 	default:
 		smtAssert(false, "Invalid SMT sort");
 	}
diff --git a/libsmtutil/Sorts.cpp b/libsmtutil/Sorts.cpp
index 543c7ba0f..9277e249d 100644
--- a/libsmtutil/Sorts.cpp
+++ b/libsmtutil/Sorts.cpp
@@ -18,6 +18,7 @@
 
 
 #include <libsmtutil/Sorts.h>
+#include <memory>
 
 using namespace std;
 
@@ -36,5 +37,6 @@ shared_ptr<IntSort> SortProvider::intSort(bool _signed)
 }
 
 shared_ptr<BitVectorSort> const SortProvider::bitVectorSort{make_shared<BitVectorSort>(256)};
+shared_ptr<RealSort> const SortProvider::realSort{make_shared<RealSort>()};
 
 }
diff --git a/libsmtutil/Sorts.h b/libsmtutil/Sorts.h
index 45668f269..9c94bface 100644
--- a/libsmtutil/Sorts.h
+++ b/libsmtutil/Sorts.h
@@ -36,7 +36,8 @@ enum class Kind
 	Function,
 	Array,
 	Sort,
-	Tuple
+	Tuple,
+	Real
 };
 
 struct Sort
@@ -65,6 +66,17 @@ struct IntSort: public Sort
 	bool isSigned;
 };
 
+struct RealSort: public Sort
+{
+	RealSort():	Sort(Kind::Real)
+	{}
+
+	bool operator==(RealSort const& _other) const
+	{
+		return Sort::operator==(_other);
+	}
+};
+
 struct BitVectorSort: public Sort
 {
 	BitVectorSort(unsigned _size):
@@ -196,6 +208,7 @@ struct SortProvider
 	static std::shared_ptr<IntSort> const sintSort;
 	static std::shared_ptr<IntSort> intSort(bool _signed = false);
 	static std::shared_ptr<BitVectorSort> const bitVectorSort;
+	static std::shared_ptr<RealSort> const realSort;
 };
 
 }
diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp
index 8d7a03392..66b4caf29 100644
--- a/libsmtutil/Z3Interface.cpp
+++ b/libsmtutil/Z3Interface.cpp
@@ -385,6 +385,8 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
 		);
 		return tupleConstructor.range();
 	}
+	case Kind::Real:
+		return m_context.real_sort();
 
 	default:
 		break;