diff --git a/regression/cbmc/real-assignments1/main.c b/regression/cbmc/real-assignments1/main.c
new file mode 100644
index 00000000000..36101d3b4e0
--- /dev/null
+++ b/regression/cbmc/real-assignments1/main.c
@@ -0,0 +1,9 @@
+int main()
+{
+  __CPROVER_real a, b;
+  a = 0;
+  b = a;
+  b++;
+  b *= 100;
+  __CPROVER_assert(0, "");
+}
diff --git a/regression/cbmc/real-assignments1/test.desc b/regression/cbmc/real-assignments1/test.desc
new file mode 100644
index 00000000000..dd038ca9cf6
--- /dev/null
+++ b/regression/cbmc/real-assignments1/test.desc
@@ -0,0 +1,7 @@
+CORE smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--trace --smt2
+^EXIT=10$
+^SIGNAL=0$
+^  b=100 \(0b1100100\)$
+--
diff --git a/regression/cbmc/real-assignments1/typecheck.desc b/regression/cbmc/real-assignments1/typecheck.desc
new file mode 100644
index 00000000000..c06ed82f381
--- /dev/null
+++ b/regression/cbmc/real-assignments1/typecheck.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+^[[:space:]]*ASSIGN main::1::b := main::1::b \* cast\(100, ℝ\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^[[:space:]]*ASSIGN main::1::b := main::1::b \* 100$
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 7f2eb517393..eeb2ed4ea25 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -135,7 +135,9 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
       " " CPROVER_PREFIX "ssize_t;\n"
     "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
     "typedef void " CPROVER_PREFIX "integer;\n"
+    "typedef void " CPROVER_PREFIX "natural;\n"
     "typedef void " CPROVER_PREFIX "rational;\n"
+    "typedef void " CPROVER_PREFIX "real;\n"
     "extern unsigned char " CPROVER_PREFIX "memory["
       CPROVER_PREFIX "constant_infinity_uint];\n"
 
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 873e857af8f..1745f1e66ae 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -102,29 +102,23 @@ bool check_c_implicit_typecast(
 
   if(src_type_id==ID_natural)
   {
-    if(dest_type.id()==ID_bool ||
-       dest_type.id()==ID_c_bool ||
-       dest_type.id()==ID_integer ||
-       dest_type.id()==ID_real ||
-       dest_type.id()==ID_complex ||
-       dest_type.id()==ID_unsignedbv ||
-       dest_type.id()==ID_signedbv ||
-       dest_type.id()==ID_floatbv ||
-       dest_type.id()==ID_complex)
+    if(
+      dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
+      dest_type.id() == ID_integer || dest_type.id() == ID_rational ||
+      dest_type.id() == ID_real || dest_type.id() == ID_complex ||
+      dest_type.id() == ID_unsignedbv || dest_type.id() == ID_signedbv ||
+      dest_type.id() == ID_floatbv || dest_type.id() == ID_complex)
       return false;
   }
   else if(src_type_id==ID_integer)
   {
-    if(dest_type.id()==ID_bool ||
-       dest_type.id()==ID_c_bool ||
-       dest_type.id()==ID_real ||
-       dest_type.id()==ID_complex ||
-       dest_type.id()==ID_unsignedbv ||
-       dest_type.id()==ID_signedbv ||
-       dest_type.id()==ID_floatbv ||
-       dest_type.id()==ID_fixedbv ||
-       dest_type.id()==ID_pointer ||
-       dest_type.id()==ID_complex)
+    if(
+      dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
+      dest_type.id() == ID_rational || dest_type.id() == ID_real ||
+      dest_type.id() == ID_complex || dest_type.id() == ID_unsignedbv ||
+      dest_type.id() == ID_signedbv || dest_type.id() == ID_floatbv ||
+      dest_type.id() == ID_fixedbv || dest_type.id() == ID_pointer ||
+      dest_type.id() == ID_complex)
       return false;
   }
   else if(src_type_id==ID_real)
@@ -139,12 +133,11 @@ bool check_c_implicit_typecast(
   }
   else if(src_type_id==ID_rational)
   {
-    if(dest_type.id()==ID_bool ||
-       dest_type.id()==ID_c_bool ||
-       dest_type.id()==ID_complex ||
-       dest_type.id()==ID_floatbv ||
-       dest_type.id()==ID_fixedbv ||
-       dest_type.id()==ID_complex)
+    if(
+      dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
+      dest_type.id() == ID_real || dest_type.id() == ID_complex ||
+      dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
+      dest_type.id() == ID_complex)
       return false;
   }
   else if(src_type_id==ID_bool)
@@ -415,6 +408,8 @@ c_typecastt::c_typet c_typecastt::get_c_type(
   }
   else if(type.id() == ID_integer)
     return INTEGER;
+  else if(type.id() == ID_natural)
+    return NATURAL;
 
   return OTHER;
 }
@@ -454,6 +449,9 @@ void c_typecastt::implicit_typecast_arithmetic(
   case RATIONAL:   new_type=rational_typet(); break;
   case REAL:       new_type=real_typet(); break;
   case INTEGER:    new_type=integer_typet(); break;
+  case NATURAL:
+    new_type = natural_typet();
+    break;
   case COMPLEX:
   case OTHER:
   case VOIDPTR:
diff --git a/src/ansi-c/c_typecast.h b/src/ansi-c/c_typecast.h
index 9585d99b7cb..7c7d536f522 100644
--- a/src/ansi-c/c_typecast.h
+++ b/src/ansi-c/c_typecast.h
@@ -75,19 +75,35 @@ class c_typecastt
 
   // these are in promotion order
 
-  enum c_typet { BOOL,
-                 CHAR, UCHAR,
-                 SHORT, USHORT,
-                 INT, UINT,
-                 LONG, ULONG,
-                 LONGLONG, ULONGLONG,
-                 LARGE_SIGNED_INT, LARGE_UNSIGNED_INT,
-                 INTEGER, // these are unbounded integers, non-standard
-                 FIXEDBV, // fixed-point, non-standard
-                 SINGLE, DOUBLE, LONGDOUBLE, FLOAT128, // float
-                 RATIONAL, REAL, // infinite precision, non-standard
-                 COMPLEX,
-                 VOIDPTR, PTR, OTHER };
+  enum c_typet
+  {
+    BOOL,
+    CHAR,
+    UCHAR,
+    SHORT,
+    USHORT,
+    INT,
+    UINT,
+    LONG,
+    ULONG,
+    LONGLONG,
+    ULONGLONG,
+    LARGE_SIGNED_INT,
+    LARGE_UNSIGNED_INT,
+    INTEGER, // these are unbounded integers, non-standard
+    NATURAL, // these are unbounded natural numbers, non-standard
+    FIXEDBV, // fixed-point, non-standard
+    SINGLE,
+    DOUBLE,
+    LONGDOUBLE,
+    FLOAT128, // float
+    RATIONAL,
+    REAL, // infinite precision, non-standard
+    COMPLEX,
+    VOIDPTR,
+    PTR,
+    OTHER
+  };
 
   c_typet get_c_type(const typet &type) const;
 
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 02e50709308..fa66b1dd238 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -1626,6 +1626,14 @@ void c_typecheck_baset::typecheck_typedef_type(typet &type)
   {
     type=integer_typet();
   }
+  else if(symbol.base_name == CPROVER_PREFIX "natural")
+  {
+    type = natural_typet();
+  }
+  else if(symbol.base_name == CPROVER_PREFIX "real")
+  {
+    type = real_typet();
+  }
 }
 
 void c_typecheck_baset::adjust_function_parameter(typet &type) const
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index ae1ec2b98dc..fd3b549667b 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -246,11 +246,11 @@ std::string expr2ct::convert_rec(
   {
     return q + CPROVER_PREFIX + "string" + d;
   }
-  else if(src.id()==ID_natural ||
-          src.id()==ID_integer ||
-          src.id()==ID_rational)
+  else if(
+    src.id() == ID_natural || src.id() == ID_integer ||
+    src.id() == ID_rational || src.id() == ID_real)
   {
-    return q+src.id_string()+d;
+    return q + CPROVER_PREFIX + src.id_string() + d;
   }
   else if(src.id()==ID_empty)
   {
@@ -1780,9 +1780,9 @@ std::string expr2ct::convert_constant(
   const irep_idt value=src.get_value();
   std::string dest;
 
-  if(type.id()==ID_integer ||
-     type.id()==ID_natural ||
-     type.id()==ID_rational)
+  if(
+    type.id() == ID_integer || type.id() == ID_natural ||
+    type.id() == ID_rational || type.id() == ID_real)
   {
     dest=id2string(value);
   }
@@ -1821,8 +1821,6 @@ std::string expr2ct::convert_constant(
     else
       return "/*enum*/" + value_as_string;
   }
-  else if(type.id()==ID_rational)
-    return convert_norep(src, precedence);
   else if(type.id()==ID_bv)
   {
     // not C
diff --git a/src/util/Makefile b/src/util/Makefile
index 1e33ebc73db..44d5d307fd9 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -66,6 +66,7 @@ SRC = arith_tools.cpp \
       prefix_filter.cpp \
       rational.cpp \
       rational_tools.cpp \
+      real.cpp \
       ref_expr_set.cpp \
       refined_string_type.cpp \
       rename.cpp \
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
index 4b14ec6ec7f..3b7c5b0f1ae 100644
--- a/src/util/arith_tools.cpp
+++ b/src/util/arith_tools.cpp
@@ -103,7 +103,7 @@ constant_exprt from_integer(
 {
   const irep_idt &type_id=type.id();
 
-  if(type_id==ID_integer)
+  if(type_id == ID_integer || type_id == ID_rational || type_id == ID_real)
   {
     return constant_exprt(integer2string(int_value), type);
   }
diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp
index 11560c150ad..25b7fa5b975 100644
--- a/src/util/format_type.cpp
+++ b/src/util/format_type.cpp
@@ -100,6 +100,8 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
     return os << "\xe2\x84\x95"; // u+2115, 'N'
   else if(id == ID_rational)
     return os << "\xe2\x84\x9a"; // u+211A, 'Q'
+  else if(id == ID_real)
+    return os << "\xe2\x84\x9d"; // u+211D, 'R'
   else if(id == ID_mathematical_function)
   {
     const auto &mathematical_function = to_mathematical_function_type(type);
diff --git a/src/util/real.cpp b/src/util/real.cpp
new file mode 100644
index 00000000000..3fb15a9f5fb
--- /dev/null
+++ b/src/util/real.cpp
@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Real Numbers
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+/// \file
+/// Real Numbers
+
+#include "real.h"
+
+realt &realt::operator-()
+{
+  integral.negate();
+  return *this;
+}
+
+std::ostream &operator<<(std::ostream &out, const realt &a)
+{
+  return out << a.get_integral() << '.' << a.get_fractional();
+}
diff --git a/src/util/real.h b/src/util/real.h
new file mode 100644
index 00000000000..a27e3c019c3
--- /dev/null
+++ b/src/util/real.h
@@ -0,0 +1,53 @@
+/*******************************************************************\
+
+Module: Real Numbers
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_REAL_H
+#define CPROVER_UTIL_REAL_H
+
+#include "mp_arith.h"
+
+class realt
+{
+protected:
+  mp_integer integral, fractional;
+
+public:
+  // constructors
+  realt() : integral(0), fractional(0)
+  {
+  }
+  explicit realt(const mp_integer &i) : integral(i), fractional(0)
+  {
+  }
+
+  realt &operator-();
+
+  bool operator==(const realt &n) const
+  {
+    return integral == n.integral && fractional == n.fractional;
+  }
+
+  bool operator!=(const realt &n) const
+  {
+    return integral != n.integral || fractional != n.fractional;
+  }
+
+  const mp_integer &get_integral() const
+  {
+    return integral;
+  }
+
+  const mp_integer &get_fractional() const
+  {
+    return fractional;
+  }
+};
+
+std::ostream &operator<<(std::ostream &out, const realt &a);
+
+#endif // CPROVER_UTIL_REAL_H
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 266de986ac4..95dd3979976 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1035,11 +1035,11 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
         return make_boolean_expr(int_value != 0);
       }
 
-      if(expr_type_id==ID_unsignedbv ||
-         expr_type_id==ID_signedbv ||
-         expr_type_id==ID_c_enum ||
-         expr_type_id==ID_c_bit_field ||
-         expr_type_id==ID_integer)
+      if(
+        expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
+        expr_type_id == ID_c_enum || expr_type_id == ID_c_bit_field ||
+        expr_type_id == ID_integer || expr_type_id == ID_natural ||
+        expr_type_id == ID_rational || expr_type_id == ID_real)
       {
         return from_integer(int_value, expr_type);
       }
@@ -1189,6 +1189,11 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
         rationalt r(int_value);
         return from_rational(r);
       }
+
+      if(expr_type_id == ID_real)
+      {
+        return from_integer(int_value, expr_type);
+      }
     }
     else if(op_type_id==ID_fixedbv)
     {