diff --git a/regression/ebmc/smv-word-level/verilog1.desc b/regression/ebmc/smv-word-level/verilog1.desc
index 33aacafe..d4dfef29 100644
--- a/regression/ebmc/smv-word-level/verilog1.desc
+++ b/regression/ebmc/smv-word-level/verilog1.desc
@@ -6,7 +6,7 @@ verilog1.sv
 ^INIT main\.x = 0ud32_0$
 ^INVAR Verilog::main\.x_aux0 = main\.x \+ 0ud32_1$
 ^TRANS next\(main\.x\) = Verilog::main\.x_aux0$
-^LTLSPEC F main\.x = 0sd32_10$
+^LTLSPEC F main\.x = unsigned\(0sd32_10\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/smv-word-level/verilog2.desc b/regression/ebmc/smv-word-level/verilog2.desc
new file mode 100644
index 00000000..9d099e00
--- /dev/null
+++ b/regression/ebmc/smv-word-level/verilog2.desc
@@ -0,0 +1,19 @@
+CORE
+verilog2.sv
+--smv-word-level
+^MODULE main$
+^INIT main\.sw1 = extend\(signed\(main\.ui\), 24\)$
+^INIT main\.sw2 = extend\(main\.si, 24\)$
+^INIT main\.uw1 = extend\(main\.ui, 24\)$
+^INIT main\.uw2 = unsigned\(extend\(main\.si, 24\)\)$
+^INIT main\.sn1 = signed\(resize\(main\.ui, 4\)\)$
+^INIT main\.sn2 = signed\(resize\(unsigned\(main.si\), 4\)\)$
+^INIT main\.un1 = resize\(main\.ui, 4\)$
+^INIT main\.un2 = resize\(unsigned\(main\.si\), 4\)$
+^INIT main\.sb1 = signed\(main\.ui\)$
+^INIT main\.sb2 = main\.si$
+^INIT main\.ub1 = main\.ui$
+^INIT main\.ub2 = unsigned\(main\.si\)$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc/smv-word-level/verilog2.sv b/regression/ebmc/smv-word-level/verilog2.sv
new file mode 100644
index 00000000..4d40d5fd
--- /dev/null
+++ b/regression/ebmc/smv-word-level/verilog2.sv
@@ -0,0 +1,21 @@
+module main(input clk, input signed [7:0] si, input unsigned [7:0] ui);
+
+  // enlarge
+  wire signed [31:0] sw1 = ui;   // unsigned 8 to signed 32
+  wire signed [31:0] sw2 = si;   // signed 8 to signed 32
+  wire unsigned [31:0] uw1 = ui; // unsigned 8 to unsigned 32
+  wire unsigned [31:0] uw2 = si; // signed 8 to unsigned 32
+
+  // shrink
+  wire signed [3:0] sn1 = ui;   // unsigned 8 to signed 4
+  wire signed [3:0] sn2 = si;   // signed 8 to signed 4
+  wire unsigned [3:0] un1 = ui; // unsigned 8 to unsigned 4
+  wire unsigned [3:0] un2 = si; // signed 8 to unsigned 4
+
+  // same size
+  wire signed [7:0] sb1 = ui;   // unsigned 8 to signed 8
+  wire signed [7:0] sb2 = si;   // signed 8 to signed 8
+  wire unsigned [7:0] ub1 = ui; // unsigned 8 to unsigned 8
+  wire unsigned [7:0] ub2 = si; // signed 8 to unsigned 8
+
+endmodule
diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp
index 02476ce1..2981504d 100644
--- a/src/smvlang/expr2smv.cpp
+++ b/src/smvlang/expr2smv.cpp
@@ -9,6 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "expr2smv.h"
 #include "expr2smv_class.h"
 
+#include <util/mathematical_types.h>
+
+#include "smv_expr.h"
+
 /*******************************************************************\
 
 Function: expr2smvt::convert_nondet_choice
@@ -221,6 +225,124 @@ expr2smvt::resultt expr2smvt::convert_function_application(
 
 /*******************************************************************\
 
+Function: expr2smvt::convert_typecast
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2smvt::resultt expr2smvt::convert_typecast(const typecast_exprt &expr)
+{
+  // typecasts can repesent a variety of functions
+  auto &src_type = expr.op().type();
+  auto &dest_type = expr.type();
+
+  if(src_type.id() == ID_unsignedbv && dest_type.id() == ID_signedbv)
+  {
+    // unsigned to signed
+    auto src_width = to_unsignedbv_type(src_type).get_width();
+    auto dest_width = to_signedbv_type(dest_type).get_width();
+
+    if(src_width == dest_width)
+    {
+      // signedness change only
+      return convert_rec(smv_signed_cast_exprt{expr.op(), dest_type});
+    }
+    else if(dest_width > src_width)
+    {
+      // Signedness _and_ width change. First go to signed, then extend.
+      return convert_rec(smv_extend_exprt{
+        smv_signed_cast_exprt{expr.op(), signedbv_typet{src_width}},
+        dest_width - src_width,
+        dest_type});
+    }
+    else
+    {
+      // First shrink, then go signed.
+      return convert_rec(smv_signed_cast_exprt{
+        smv_resize_exprt{expr.op(), dest_width, unsignedbv_typet{dest_width}},
+        dest_type});
+    }
+  }
+  else if(src_type.id() == ID_signedbv && dest_type.id() == ID_unsignedbv)
+  {
+    // signed to unsigned
+    auto src_width = to_signedbv_type(src_type).get_width();
+    auto dest_width = to_unsignedbv_type(dest_type).get_width();
+
+    if(
+      to_signedbv_type(src_type).get_width() ==
+      to_unsignedbv_type(dest_type).get_width())
+    {
+      // signedness change only
+      return convert_rec(smv_unsigned_cast_exprt{expr.op(), dest_type});
+    }
+    else if(dest_width > src_width)
+    {
+      // Signedness _and_ width change.
+      // First enlarge, then go unsigned.
+      return convert_rec(smv_unsigned_cast_exprt{
+        smv_extend_exprt{
+          expr.op(), dest_width - src_width, signedbv_typet{dest_width}},
+        dest_type});
+    }
+    else
+    {
+      // First go unsigned, then shrink
+      return convert_rec(smv_resize_exprt{
+        smv_unsigned_cast_exprt{expr.op(), unsignedbv_typet{src_width}},
+        dest_width,
+        dest_type});
+    }
+  }
+  else if(src_type.id() == ID_signedbv && dest_type.id() == ID_signedbv)
+  {
+    // signed to signed, width change.
+    auto src_width = to_signedbv_type(src_type).get_width();
+    auto dest_width = to_signedbv_type(dest_type).get_width();
+    if(dest_width > src_width)
+    {
+      // enlarge using extend
+      return convert_rec(
+        smv_extend_exprt{expr.op(), dest_width - src_width, dest_type});
+    }
+    else
+    {
+      // Note that SMV's resize(...) preserves the sign bit, unlike our typecast.
+      // We therefore first go unsigned, then resize, then go signed again.
+      return convert_rec(smv_signed_cast_exprt{
+        smv_resize_exprt{
+          smv_unsigned_cast_exprt{expr.op(), unsignedbv_typet{src_width}},
+          dest_width,
+          unsignedbv_typet{dest_width}},
+        dest_type});
+    }
+  }
+  else if(src_type.id() == ID_unsignedbv && dest_type.id() == ID_unsignedbv)
+  {
+    // Unsigned to unsigned, width change. Use extend when enlarging.
+    auto src_width = to_unsignedbv_type(src_type).get_width();
+    auto dest_width = to_unsignedbv_type(dest_type).get_width();
+    if(dest_width > src_width)
+    {
+      return convert_rec(
+        smv_extend_exprt{expr.op(), dest_width - src_width, dest_type});
+    }
+    else
+    {
+      return convert_rec(smv_resize_exprt{expr.op(), dest_width, dest_type});
+    }
+  }
+  else
+    return convert_norep(expr);
+}
+
+/*******************************************************************\
+
 Function: expr2smvt::convert_rtctl
 
   Inputs:
@@ -714,7 +836,7 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
 
   else if(src.id() == ID_typecast)
   {
-    return convert_rec(to_typecast_expr(src).op());
+    return convert_typecast(to_typecast_expr(src));
   }
 
   else // no SMV language expression for internal representation
diff --git a/src/smvlang/expr2smv_class.h b/src/smvlang/expr2smv_class.h
index 35b84c08..10a1c7ab 100644
--- a/src/smvlang/expr2smv_class.h
+++ b/src/smvlang/expr2smv_class.h
@@ -126,6 +126,8 @@ class expr2smvt
   resultt
   convert_function_application(const std::string &symbol, const exprt &);
 
+  resultt convert_typecast(const typecast_exprt &);
+
   resultt convert_norep(const exprt &);
 };