diff --git a/regression/verilog/expressions/cast_to_real1.desc b/regression/verilog/expressions/cast_to_real1.desc
new file mode 100644
index 00000000..935649bc
--- /dev/null
+++ b/regression/verilog/expressions/cast_to_real1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+cast_to_real1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Typechecking is failing.
diff --git a/regression/verilog/expressions/cast_to_real1.sv b/regression/verilog/expressions/cast_to_real1.sv
new file mode 100644
index 00000000..69a4ddb0
--- /dev/null
+++ b/regression/verilog/expressions/cast_to_real1.sv
@@ -0,0 +1,10 @@
+module main;
+
+  p0: assert final (real'(0) == 0.0);
+  p1: assert final (real'(1) == 1.0);
+  p2: assert final (real'(-1) == -1.0);
+  p3: assert final (real'(1'b1) == 1);
+  p4: assert final (real'('hffff_ffff_ffff_ffff) == real'('h1_0000_0000_0000_0000));
+  p5: assert final (real'(-'sh0_ffff_ffff_ffff_ffff) == real'(-'sh1_0000_0000_0000_0000));
+
+endmodule
diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp
index 1631c94f..1fdc0693 100644
--- a/src/verilog/verilog_lowering.cpp
+++ b/src/verilog/verilog_lowering.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/ieee_float.h>
+#include <util/floatbv_expr.h>
 
 #include "aval_bval_encoding.h"
 #include "verilog_bits.h"
@@ -272,7 +273,16 @@ 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 floatbv_typecast;
+    }
+    else
+      return expr;
   }
   else if(expr.id() == ID_verilog_explicit_type_cast)
   {