diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp
index 2981504d..d88610a2 100644
--- a/src/smvlang/expr2smv.cpp
+++ b/src/smvlang/expr2smv.cpp
@@ -343,6 +343,100 @@ expr2smvt::resultt expr2smvt::convert_typecast(const typecast_exprt &expr)
 
 /*******************************************************************\
 
+Function: expr2smvt::convert_zero_extend
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2smvt::resultt expr2smvt::convert_zero_extend(const zero_extend_exprt &expr)
+{
+  // these may apply to a variety of operand/result types
+  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
+    {
+      PRECONDITION(dest_width > src_width);
+
+      // Signedness _and_ width change. First extend, then go signed
+      return convert_rec(smv_signed_cast_exprt{
+        smv_extend_exprt{
+          expr.op(), dest_width - src_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(src_width == dest_width)
+    {
+      // signedness change only
+      return convert_rec(smv_unsigned_cast_exprt{expr.op(), dest_type});
+    }
+    else
+    {
+      PRECONDITION(dest_width > src_width);
+
+      // Signedness _and_ width change. First go unsigned, then enlarge.
+      return convert_rec(smv_extend_exprt{
+        smv_unsigned_cast_exprt{expr.op(), unsignedbv_typet{src_width}},
+        dest_width - src_width,
+        dest_type});
+    }
+  }
+  else if(src_type.id() == ID_signedbv && dest_type.id() == ID_signedbv)
+  {
+    // Note that SMV's resize(...) preserves the sign bit, unlike our typecast.
+    // We therefore first go unsigned, then resize, then go signed again.
+    auto src_width = to_signedbv_type(src_type).get_width();
+    auto dest_width = to_signedbv_type(dest_type).get_width();
+    PRECONDITION(dest_width >= src_width);
+    return convert_rec(smv_signed_cast_exprt{
+      smv_extend_exprt{
+        smv_unsigned_cast_exprt{expr.op(), unsignedbv_typet{src_width}},
+        dest_width - src_width,
+        unsignedbv_typet{dest_width}},
+      dest_type});
+  }
+  else if(src_type.id() == ID_unsignedbv && dest_type.id() == ID_unsignedbv)
+  {
+    // Unsigned to unsigned, possible width change.
+    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(expr.op()); // no change
+    else
+    {
+      PRECONDITION(dest_width > src_width);
+      return convert_rec(
+        smv_extend_exprt{expr.op(), dest_width - src_width, dest_type});
+    }
+  }
+  else
+    return convert_norep(expr);
+}
+
+/*******************************************************************\
+
 Function: expr2smvt::convert_rtctl
 
   Inputs:
@@ -839,6 +933,11 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
     return convert_typecast(to_typecast_expr(src));
   }
 
+  else if(src.id() == ID_zero_extend)
+  {
+    return convert_zero_extend(to_zero_extend_expr(src));
+  }
+
   else // no SMV language expression for internal representation
     return convert_norep(src);
 }
diff --git a/src/smvlang/expr2smv_class.h b/src/smvlang/expr2smv_class.h
index 10a1c7ab..63d7fa91 100644
--- a/src/smvlang/expr2smv_class.h
+++ b/src/smvlang/expr2smv_class.h
@@ -10,6 +10,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #define CPROVER_SMV_EXPR2SMV_CLASS_H
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
@@ -128,6 +129,8 @@ class expr2smvt
 
   resultt convert_typecast(const typecast_exprt &);
 
+  resultt convert_zero_extend(const zero_extend_exprt &);
+
   resultt convert_norep(const exprt &);
 };
 
diff --git a/src/verilog/aval_bval_encoding.cpp b/src/verilog/aval_bval_encoding.cpp
index 78167552..def8e76e 100644
--- a/src/verilog/aval_bval_encoding.cpp
+++ b/src/verilog/aval_bval_encoding.cpp
@@ -470,3 +470,8 @@ exprt aval_bval(const shift_exprt &expr)
   auto x = make_x(expr.type());
   return if_exprt{distance_has_xz, x, combined};
 }
+
+exprt aval_bval(const zero_extend_exprt &expr)
+{
+  abort();
+}
diff --git a/src/verilog/aval_bval_encoding.h b/src/verilog/aval_bval_encoding.h
index 5b29d238..d84938fd 100644
--- a/src/verilog/aval_bval_encoding.h
+++ b/src/verilog/aval_bval_encoding.h
@@ -65,5 +65,7 @@ exprt aval_bval(const verilog_implies_exprt &);
 exprt aval_bval(const typecast_exprt &);
 /// lowering for shifts
 exprt aval_bval(const shift_exprt &);
+/// lowering for zero extension
+exprt aval_bval(const zero_extend_exprt &);
 
 #endif
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index c79aa20d..77f9f519 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -896,6 +896,25 @@ expr2verilogt::resultt expr2verilogt::convert_explicit_size_cast(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_zero_extend
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt
+expr2verilogt::convert_zero_extend(const zero_extend_exprt &src)
+{
+  // added by the type checker; igore
+  return convert_rec(src.op());
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_index
 
   Inputs:
@@ -1664,6 +1683,9 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
   else if(src.id()==ID_typecast)
     return convert_typecast(to_typecast_expr(src));
 
+  else if(src.id() == ID_zero_extend)
+    return convert_zero_extend(to_zero_extend_expr(src));
+
   else if(src.id()==ID_and)
     return convert_binary(
       to_multi_ary_expr(src), "&&", precedence = verilog_precedencet::AND);
diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h
index fa03a76f..31272b43 100644
--- a/src/verilog/expr2verilog_class.h
+++ b/src/verilog/expr2verilog_class.h
@@ -117,6 +117,8 @@ class expr2verilogt
 
   resultt convert_typecast(const typecast_exprt &);
 
+  resultt convert_zero_extend(const zero_extend_exprt &);
+
   resultt
   convert_explicit_size_cast(const class verilog_explicit_size_cast_exprt &);
 
diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp
index 46586999..2d678ac2 100644
--- a/src/verilog/verilog_lowering.cpp
+++ b/src/verilog/verilog_lowering.cpp
@@ -615,6 +615,20 @@ exprt verilog_lowering(exprt expr)
     else
       return expr;
   }
+  else if(expr.id() == ID_zero_extend)
+  {
+    auto &zero_extend = to_zero_extend_expr(expr);
+
+    if(
+      is_four_valued(zero_extend.type()) ||
+      is_four_valued(zero_extend.op().type()))
+    {
+      // encode into aval/bval
+      return aval_bval(zero_extend);
+    }
+    else
+      return expr; // leave as is
+  }
   else
     return expr; // leave as is
 
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index a57aaf35..25c38b4d 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -2316,23 +2316,14 @@ Function: zero_extend
 
 static exprt zero_extend(const exprt &expr, const typet &type)
 {
-  auto old_width = expr.type().id() == ID_bool ? 1
-                   : expr.type().id() == ID_integer
-                     ? 32
-                     : to_bitvector_type(expr.type()).get_width();
+  exprt result = expr;
 
-  // first make unsigned
-  typet tmp_type;
+  if(expr.type().id() == ID_bool)
+    result = typecast_exprt{expr, unsignedbv_typet{1}};
+  else if(expr.type().id() == ID_integer)
+    result = typecast_exprt{expr, unsignedbv_typet{32}};
 
-  if(type.id() == ID_unsignedbv)
-    tmp_type = unsignedbv_typet{old_width};
-  else if(type.id() == ID_verilog_unsignedbv)
-    tmp_type = verilog_unsignedbv_typet{old_width};
-  else
-    PRECONDITION(false);
-
-  return typecast_exprt::conditional_cast(
-    typecast_exprt::conditional_cast(expr, tmp_type), type);
+  return zero_extend_exprt{std::move(result), type};
 }
 
 /*******************************************************************\