diff --git a/regression/verilog/expressions/signing_cast1.desc b/regression/verilog/expressions/signing_cast1.desc
index 16d684056..9d8866326 100644
--- a/regression/verilog/expressions/signing_cast1.desc
+++ b/regression/verilog/expressions/signing_cast1.desc
@@ -1,12 +1,12 @@
-KNOWNBUG
+CORE broken-smt-backend
 signing_cast1.sv
 --module main --bound 0
-^\[main\.p0\] always signed \[0:0\]'\(1'b1\) == -1: PROVED up to bound 0$
-^\[main\.p1\] always signed \[0:0\]'\(4'b1110\) == -2: PROVED up to bound 0$
-^\[main\.p2\] always signed \[0:0\]'\(4'b0111\) == 7: PROVED up to bound 0$
-^\[main\.p3\] always signed \[0:0\]'\(!0\) == -1: PROVED up to bound 0$
-^\[main\.p4\] always \[0:0\]'\(!0\) == 1: PROVED up to bound 0$
-^\[main\.p5\] always \[0:0\]'\(-1\) == 32'hFFFFFFFF: PROVED up to bound 0$
+^\[main\.p0\] always signed'\(1'b1\) == -1: PROVED up to bound 0$
+^\[main\.p1\] always signed'\(4'b1110\) == -2: PROVED up to bound 0$
+^\[main\.p2\] always signed'\(4'b0111\) == 7: PROVED up to bound 0$
+^\[main\.p3\] always signed'\(!0\) == -1: PROVED up to bound 0$
+^\[main\.p4\] always unsigned'\(!0\) == 1: PROVED up to bound 0$
+^\[main\.p5\] always unsigned'\(-1\) == 32'hFFFFFFFF: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 2f3efca0a..506c49351 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -83,8 +83,10 @@ IREP_ID_ONE(verilog_logical_equality)
 IREP_ID_ONE(verilog_logical_inequality)
 IREP_ID_ONE(verilog_wildcard_equality)
 IREP_ID_ONE(verilog_wildcard_inequality)
-IREP_ID_ONE(verilog_explicit_cast)
-IREP_ID_ONE(verilog_size_cast)
+IREP_ID_ONE(verilog_explicit_const_cast)
+IREP_ID_ONE(verilog_explicit_signing_cast)
+IREP_ID_ONE(verilog_explicit_size_cast)
+IREP_ID_ONE(verilog_explicit_type_cast)
 IREP_ID_ONE(verilog_implicit_typecast)
 IREP_ID_ONE(verilog_inside)
 IREP_ID_ONE(verilog_unique)
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index 036dc0f1b..8fdf1ebaf 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -694,7 +694,7 @@ expr2verilogt::convert_typecast(const typecast_exprt &src)
 
 /*******************************************************************\
 
-Function: expr2verilogt::convert_explicit_cast
+Function: expr2verilogt::convert_explicit_const_cast
 
   Inputs:
 
@@ -704,8 +704,47 @@ Function: expr2verilogt::convert_explicit_cast
 
 \*******************************************************************/
 
-expr2verilogt::resultt
-expr2verilogt::convert_explicit_cast(const verilog_explicit_cast_exprt &src)
+expr2verilogt::resultt expr2verilogt::convert_explicit_const_cast(
+  const verilog_explicit_const_cast_exprt &src)
+{
+  return {verilog_precedencet::MAX, "const'(" + convert_rec(src.op()).s + ')'};
+}
+
+/*******************************************************************\
+
+Function: expr2verilogt::convert_explicit_signing_cast
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt expr2verilogt::convert_explicit_signing_cast(
+  const verilog_explicit_signing_cast_exprt &src)
+{
+  std::string signing = src.is_signed() ? "signed" : "unsigned";
+
+  return {
+    verilog_precedencet::MAX, signing + "'(" + convert_rec(src.op()).s + ')'};
+}
+
+/*******************************************************************\
+
+Function: expr2verilogt::convert_explicit_type_cast
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt expr2verilogt::convert_explicit_type_cast(
+  const verilog_explicit_type_cast_exprt &src)
 {
   return {
     verilog_precedencet::MAX,
@@ -714,7 +753,7 @@ expr2verilogt::convert_explicit_cast(const verilog_explicit_cast_exprt &src)
 
 /*******************************************************************\
 
-Function: expr2verilogt::convert_size_cast
+Function: expr2verilogt::convert_explicit_size_cast
 
   Inputs:
 
@@ -724,8 +763,8 @@ Function: expr2verilogt::convert_size_cast
 
 \*******************************************************************/
 
-expr2verilogt::resultt
-expr2verilogt::convert_size_cast(const verilog_size_cast_exprt &src)
+expr2verilogt::resultt expr2verilogt::convert_explicit_size_cast(
+  const verilog_explicit_size_cast_exprt &src)
 {
   return {
     verilog_precedencet::MAX,
@@ -1490,11 +1529,19 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return convert_unary(
       to_bitnot_expr(src), "~", precedence = verilog_precedencet::NOT);
 
-  else if(src.id() == ID_verilog_explicit_cast)
-    return convert_explicit_cast(to_verilog_explicit_cast_expr(src));
+  else if(src.id() == ID_verilog_explicit_const_cast)
+    return convert_explicit_const_cast(
+      to_verilog_explicit_const_cast_expr(src));
+
+  else if(src.id() == ID_verilog_explicit_size_cast)
+    return convert_explicit_size_cast(to_verilog_explicit_size_cast_expr(src));
+
+  else if(src.id() == ID_verilog_explicit_signing_cast)
+    return convert_explicit_signing_cast(
+      to_verilog_explicit_signing_cast_expr(src));
 
-  else if(src.id() == ID_verilog_size_cast)
-    return convert_size_cast(to_verilog_size_cast_expr(src));
+  else if(src.id() == ID_verilog_explicit_type_cast)
+    return convert_explicit_type_cast(to_verilog_explicit_type_cast_expr(src));
 
   else if(src.id()==ID_typecast)
     return convert_typecast(to_typecast_expr(src));
diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h
index 4a75c3d9c..15896451e 100644
--- a/src/verilog/expr2verilog_class.h
+++ b/src/verilog/expr2verilog_class.h
@@ -105,11 +105,19 @@ class expr2verilogt
 
   resultt convert_constant(const constant_exprt &, verilog_precedencet &);
 
-  resultt convert_explicit_cast(const class verilog_explicit_cast_exprt &);
+  resultt
+  convert_explicit_const_cast(const class verilog_explicit_const_cast_exprt &);
+
+  resultt convert_explicit_signing_cast(
+    const class verilog_explicit_signing_cast_exprt &);
+
+  resultt
+  convert_explicit_type_cast(const class verilog_explicit_type_cast_exprt &);
 
   resultt convert_typecast(const typecast_exprt &);
 
-  resultt convert_size_cast(const class verilog_size_cast_exprt &);
+  resultt
+  convert_explicit_size_cast(const class verilog_explicit_size_cast_exprt &);
 
   resultt
   convert_concatenation(const concatenation_exprt &, verilog_precedencet);
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index 7050657c0..ccff7994c 100644
--- a/src/verilog/parser.y
+++ b/src/verilog/parser.y
@@ -1419,11 +1419,27 @@ lifetime:
 
 casting_type:
 	  simple_type
+		{
+		  init($$, ID_verilog_explicit_type_cast);
+		  stack_expr($$).type() = stack_type($1);
+		}
 	| constant_primary
-		{ init($$, ID_verilog_size_cast); mto($$, $1); }
+		{ init($$, ID_verilog_explicit_size_cast); mto($$, $1); }
 	| signing
+		{
+		  init($$, ID_verilog_explicit_signing_cast);
+		  stack_expr($$).type() = stack_type($1);
+		}
 	| TOK_STRING
+		{
+		  init($$, ID_verilog_explicit_type_cast);
+		  stack_expr($$).type() = stack_type($1);
+		}
 	| TOK_CONST
+		{
+		  init($$, ID_verilog_explicit_const_cast);
+		  stack_expr($$).type() = stack_type($1);
+		}
 	;
 
 data_type:
@@ -4044,18 +4060,7 @@ time_literal: TOK_TIME_LITERAL
 
 cast:
 	  casting_type '\'' '(' expression ')'
-		{ if(stack_expr($1).id() == ID_verilog_size_cast)
-		  {
-		    $$ = $1; 
-		    mto($$, $4);
-		  }
-		  else
-		  {
-		    init($$, ID_verilog_explicit_cast);
-		    stack_expr($$).type() = stack_type($1);
-		    mto($$, $4);
-		  }
-		}
+		{ $$ = $1; mto($$, $4); }
 	;
 
 // System Verilog standard 1800-2017
diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h
index dd03936f2..bcb76b810 100644
--- a/src/verilog/verilog_expr.h
+++ b/src/verilog/verilog_expr.h
@@ -2462,13 +2462,13 @@ inline verilog_udpt &to_verilog_udp(irept &irep)
 }
 
 /// size'(expression)
-class verilog_size_cast_exprt : public binary_exprt
+class verilog_explicit_size_cast_exprt : public binary_exprt
 {
 public:
-  verilog_size_cast_exprt(exprt __size, exprt __op, typet __type)
+  verilog_explicit_size_cast_exprt(exprt __size, exprt __op, typet __type)
     : binary_exprt(
         std::move(__size),
-        ID_verilog_size_cast,
+        ID_verilog_explicit_size_cast,
         std::move(__op),
         std::move(__type))
   {
@@ -2501,24 +2501,97 @@ class verilog_size_cast_exprt : public binary_exprt
   }
 };
 
-inline const verilog_size_cast_exprt &
-to_verilog_size_cast_expr(const exprt &expr)
+inline const verilog_explicit_size_cast_exprt &
+to_verilog_explicit_size_cast_expr(const exprt &expr)
 {
-  verilog_size_cast_exprt::check(expr);
-  return static_cast<const verilog_size_cast_exprt &>(expr);
+  verilog_explicit_size_cast_exprt::check(expr);
+  return static_cast<const verilog_explicit_size_cast_exprt &>(expr);
 }
 
-inline verilog_size_cast_exprt &to_verilog_size_cast_expr(exprt &expr)
+inline verilog_explicit_size_cast_exprt &
+to_verilog_explicit_size_cast_expr(exprt &expr)
 {
-  verilog_size_cast_exprt::check(expr);
-  return static_cast<verilog_size_cast_exprt &>(expr);
+  verilog_explicit_size_cast_exprt::check(expr);
+  return static_cast<verilog_explicit_size_cast_exprt &>(expr);
 }
 
-class verilog_explicit_cast_exprt : public unary_exprt
+class verilog_explicit_const_cast_exprt : public unary_exprt
 {
 public:
-  verilog_explicit_cast_exprt(exprt __op, typet __type)
-    : unary_exprt(ID_verilog_explicit_cast, std::move(__op), std::move(__type))
+  verilog_explicit_const_cast_exprt(exprt __op, typet __type)
+    : unary_exprt(
+        ID_verilog_explicit_const_cast,
+        std::move(__op),
+        std::move(__type))
+  {
+  }
+
+  exprt lower() const
+  {
+    return typecast_exprt{op(), type()};
+  }
+};
+
+inline const verilog_explicit_const_cast_exprt &
+to_verilog_explicit_const_cast_expr(const exprt &expr)
+{
+  verilog_explicit_const_cast_exprt::check(expr);
+  return static_cast<const verilog_explicit_const_cast_exprt &>(expr);
+}
+
+inline verilog_explicit_const_cast_exprt &
+to_verilog_explicit_const_cast_expr(exprt &expr)
+{
+  verilog_explicit_const_cast_exprt::check(expr);
+  return static_cast<verilog_explicit_const_cast_exprt &>(expr);
+}
+
+class verilog_explicit_signing_cast_exprt : public unary_exprt
+{
+public:
+  verilog_explicit_signing_cast_exprt(exprt __op, typet __type)
+    : unary_exprt(
+        ID_verilog_explicit_signing_cast,
+        std::move(__op),
+        std::move(__type))
+  {
+  }
+
+  bool is_signed() const
+  {
+    auto &dest_type = type();
+    return dest_type.id() == ID_signedbv ||
+           dest_type.id() == ID_verilog_signedbv;
+  }
+
+  exprt lower() const
+  {
+    return typecast_exprt{op(), type()};
+  }
+};
+
+inline const verilog_explicit_signing_cast_exprt &
+to_verilog_explicit_signing_cast_expr(const exprt &expr)
+{
+  verilog_explicit_signing_cast_exprt::check(expr);
+  return static_cast<const verilog_explicit_signing_cast_exprt &>(expr);
+}
+
+inline verilog_explicit_signing_cast_exprt &
+to_verilog_explicit_signing_cast_expr(exprt &expr)
+{
+  verilog_explicit_signing_cast_exprt::check(expr);
+  return static_cast<verilog_explicit_signing_cast_exprt &>(expr);
+}
+
+class verilog_explicit_type_cast_exprt : public unary_exprt
+{
+public:
+  verilog_explicit_type_cast_exprt(exprt __op, typet __type)
+    : unary_exprt(
+        ID_verilog_explicit_type_cast,
+        std::move(__op),
+        std::move(__type))
   {
   }
 
@@ -2528,17 +2601,18 @@ class verilog_explicit_cast_exprt : public unary_exprt
   }
 };
 
-inline const verilog_explicit_cast_exprt &
-to_verilog_explicit_cast_expr(const exprt &expr)
+inline const verilog_explicit_type_cast_exprt &
+to_verilog_explicit_type_cast_expr(const exprt &expr)
 {
-  verilog_explicit_cast_exprt::check(expr);
-  return static_cast<const verilog_explicit_cast_exprt &>(expr);
+  verilog_explicit_type_cast_exprt::check(expr);
+  return static_cast<const verilog_explicit_type_cast_exprt &>(expr);
 }
 
-inline verilog_explicit_cast_exprt &to_verilog_explicit_cast_expr(exprt &expr)
+inline verilog_explicit_type_cast_exprt &
+to_verilog_explicit_type_cast_expr(exprt &expr)
 {
-  verilog_explicit_cast_exprt::check(expr);
-  return static_cast<verilog_explicit_cast_exprt &>(expr);
+  verilog_explicit_type_cast_exprt::check(expr);
+  return static_cast<verilog_explicit_type_cast_exprt &>(expr);
 }
 
 class verilog_implicit_typecast_exprt : public unary_exprt
diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp
index 8e957b0f3..1631c94fc 100644
--- a/src/verilog/verilog_lowering.cpp
+++ b/src/verilog/verilog_lowering.cpp
@@ -274,13 +274,17 @@ exprt verilog_lowering(exprt expr)
 
     return expr;
   }
-  else if(expr.id() == ID_verilog_explicit_cast)
+  else if(expr.id() == ID_verilog_explicit_type_cast)
   {
-    return to_verilog_explicit_cast_expr(expr).lower();
+    return to_verilog_explicit_type_cast_expr(expr).lower();
   }
-  else if(expr.id() == ID_verilog_size_cast)
+  else if(expr.id() == ID_verilog_explicit_signing_cast)
   {
-    return to_verilog_size_cast_expr(expr).lower();
+    return to_verilog_explicit_signing_cast_expr(expr).lower();
+  }
+  else if(expr.id() == ID_verilog_explicit_size_cast)
+  {
+    return to_verilog_explicit_size_cast_expr(expr).lower();
   }
   else if(
     expr.id() == ID_verilog_streaming_concatenation_left_to_right ||
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index 39054e148..37fc4dcd4 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -2306,13 +2306,72 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     no_bool_ops(expr);
     expr.type() = expr.op().type();
   }
-  else if(expr.id() == ID_verilog_explicit_cast)
+  else if(expr.id() == ID_verilog_explicit_const_cast)
+  {
+    // SystemVerilog has got const'(expr).
+    // This is an explicit type cast.
+    convert_expr(expr.op());
+    expr.type() = expr.op().type();
+  }
+  else if(expr.id() == ID_verilog_explicit_type_cast)
   {
     // SystemVerilog has got type'(expr). This is an explicit
     // type cast.
     convert_expr(expr.op());
     expr.type() = elaborate_type(expr.type());
   }
+  else if(expr.id() == ID_verilog_explicit_signing_cast)
+  {
+    // SystemVerilog has got signed'(expr) and unsigned'(expr).
+    // This is an explicit type cast.
+    convert_expr(expr.op());
+    const auto &old_type = expr.op().type();
+    const auto dest_type = expr.type().id();
+    PRECONDITION(dest_type == ID_signed || dest_type == ID_unsigned);
+
+    if(old_type.id() == ID_signedbv)
+    {
+      if(dest_type == ID_unsigned)
+        expr.type() = unsignedbv_typet{to_signedbv_type(old_type).get_width()};
+      else
+        expr.type() = old_type; // leave as is
+    }
+    else if(old_type.id() == ID_verilog_signedbv)
+    {
+      if(dest_type == ID_unsigned)
+        expr.type() = verilog_unsignedbv_typet{
+          to_verilog_signedbv_type(old_type).get_width()};
+      else
+        expr.type() = old_type; // leave as is
+    }
+    else if(old_type.id() == ID_unsignedbv)
+    {
+      if(dest_type == ID_signed)
+        expr.type() = signedbv_typet{to_unsignedbv_type(old_type).get_width()};
+      else
+        expr.type() = old_type; // leave as is
+    }
+    else if(old_type.id() == ID_verilog_unsignedbv)
+    {
+      if(dest_type == ID_signed)
+        expr.type() = verilog_signedbv_typet{
+          to_verilog_unsignedbv_type(old_type).get_width()};
+      else
+        expr.type() = old_type; // leave as is
+    }
+    else if(old_type.id() == ID_bool)
+    {
+      if(dest_type == ID_signed)
+        expr.type() = signedbv_typet{1};
+      else
+        expr.type() = old_type; // leave as is
+    }
+    else
+    {
+      throw errort().with_location(expr.source_location())
+        << "signing cast expects a scalar operand";
+    }
+  }
   else if(expr.id() == ID_verilog_implicit_typecast)
   {
     // We generate implict casts during elaboration.
@@ -2785,7 +2844,7 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     return convert_hierarchical_identifier(
       to_hierarchical_identifier_expr(std::move(expr)));
   }
-  else if(expr.id() == ID_verilog_size_cast)
+  else if(expr.id() == ID_verilog_explicit_size_cast)
   {
     // SystemVerilog has got expr'(expr). This is an explicit
     // type cast, to change the size (in bits) of the rhs to the