diff --git a/regression/verilog/expressions/cast_to_real1.desc b/regression/verilog/expressions/cast_to_real1.desc
new file mode 100644
index 00000000..43edd4b1
--- /dev/null
+++ b/regression/verilog/expressions/cast_to_real1.desc
@@ -0,0 +1,8 @@
+CORE
+cast_to_real1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/expressions/cast_to_real1.sv b/regression/verilog/expressions/cast_to_real1.sv
new file mode 100644
index 00000000..9f354b54
--- /dev/null
+++ b/regression/verilog/expressions/cast_to_real1.sv
@@ -0,0 +1,11 @@
+module main;
+
+  // no rounding
+  p0: assert final (real'(0) == 0.0);
+  p1: assert final (real'(1) == 1.0);
+
+  // rounding
+  p2: assert final (real'('hffff_ffff_ffff_ffff) == real'('h1_0000_0000_0000_0000));
+  p3: assert final (real'(-'sh0_ffff_ffff_ffff_ffff) == real'(-'sh1_0000_0000_0000_0000));
+
+endmodule
diff --git a/regression/verilog/expressions/cast_to_real2.desc b/regression/verilog/expressions/cast_to_real2.desc
new file mode 100644
index 00000000..62688441
--- /dev/null
+++ b/regression/verilog/expressions/cast_to_real2.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+cast_to_real2.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Typechecking yields inconsistent types.
diff --git a/regression/verilog/expressions/cast_to_real2.sv b/regression/verilog/expressions/cast_to_real2.sv
new file mode 100644
index 00000000..888febf9
--- /dev/null
+++ b/regression/verilog/expressions/cast_to_real2.sv
@@ -0,0 +1,5 @@
+module main;
+
+  p0: assert final (real'(-1) == -1.0);
+
+endmodule
diff --git a/regression/verilog/expressions/cast_to_real3.desc b/regression/verilog/expressions/cast_to_real3.desc
new file mode 100644
index 00000000..eba51338
--- /dev/null
+++ b/regression/verilog/expressions/cast_to_real3.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+cast_to_real3.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The flattening solver fails with a width error.
diff --git a/regression/verilog/expressions/cast_to_real3.sv b/regression/verilog/expressions/cast_to_real3.sv
new file mode 100644
index 00000000..bd035901
--- /dev/null
+++ b/regression/verilog/expressions/cast_to_real3.sv
@@ -0,0 +1,5 @@
+module main;
+
+  p0: assert final (real'(1'b1) == 1);
+
+endmodule
diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp
index 1631c94f..67f85b71 100644
--- a/src/verilog/verilog_lowering.cpp
+++ b/src/verilog/verilog_lowering.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/c_types.h>
+#include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 
 #include "aval_bval_encoding.h"
@@ -272,7 +273,18 @@ exprt verilog_lowering(exprt expr)
       }
     }
 
-    return expr;
+    // Cast to float? Turn into floatbv_typecast,
+    // with rounding mode.
+    if(typecast_expr.type().id() == ID_floatbv)
+    {
+      auto rm = ieee_floatt::rounding_mode_expr(
+        ieee_floatt::rounding_modet::ROUND_TO_EVEN);
+      auto floatbv_typecast =
+        floatbv_typecast_exprt{typecast_expr.op(), rm, typecast_expr.type()};
+      return std::move(floatbv_typecast);
+    }
+    else
+      return expr;
   }
   else if(expr.id() == ID_verilog_explicit_type_cast)
   {