diff --git a/regression/cbmc/Pointer_cast_extend/main.c b/regression/cbmc/Pointer_cast_extend/main.c
new file mode 100644
index 00000000000..f2302e07440
--- /dev/null
+++ b/regression/cbmc/Pointer_cast_extend/main.c
@@ -0,0 +1,23 @@
+int nondet_int(void);
+unsigned nondet_unsigned(void);
+
+int main(void)
+{
+  // signed int to wider pointer: sign-extends
+  int i = nondet_int();
+  __CPROVER_assume(i < 0 && i > -5);
+  char *p1 = (char *)i;
+  unsigned long u1 = (unsigned long)p1;
+  __CPROVER_assert(
+    u1 > 0xFFFFFFFFul, "signed int to wider pointer sign-extends");
+
+  // unsigned int to wider pointer: zero-extends
+  unsigned v = nondet_unsigned();
+  __CPROVER_assume(v > 0x80000000u && v < 0x80001000u);
+  char *p2 = (char *)v;
+  unsigned long u2 = (unsigned long)p2;
+  __CPROVER_assert(
+    u2 < 0x100000000ul, "unsigned to wider pointer zero-extends");
+
+  return 0;
+}
diff --git a/regression/cbmc/Pointer_cast_extend/test.desc b/regression/cbmc/Pointer_cast_extend/test.desc
new file mode 100644
index 00000000000..a5790e40f01
--- /dev/null
+++ b/regression/cbmc/Pointer_cast_extend/test.desc
@@ -0,0 +1,8 @@
+CORE broken-cprover-smt-backend
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 52482e8b060..750116b4458 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -403,11 +403,23 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
     {
       // Cast from a bitvector type to pointer.
-      // We just do a zero extension.
+      // Extend according to the signedness of the source type (GCC
+      // semantics for implementation-defined integer-to-pointer
+      // conversion).
 
-      const bvt &op_bv=convert_bv(op);
+      const bvt &op_bv = convert_bv(op);
 
-      return bv_utils.zero_extension(op_bv, bits);
+      if(
+        op_type.id() == ID_signedbv ||
+        (op_type.id() == ID_c_enum &&
+         to_c_enum_type(op_type).underlying_type().id() == ID_signedbv))
+      {
+        return bv_utils.sign_extension(op_bv, bits);
+      }
+      else
+      {
+        return bv_utils.zero_extension(op_bv, bits);
+      }
     }
   }
   else if(expr.id()==ID_if)
@@ -719,10 +731,10 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     // pointer to int
     bvt op0 = convert_bv(to_typecast_expr(expr).op());
 
-    // squeeze it in!
-    std::size_t width=boolbv_width(expr.type());
+    // GCC sign-extends pointers converted to wider integer types.
+    std::size_t width = boolbv_width(expr.type());
 
-    return bv_utils.zero_extension(op0, width);
+    return bv_utils.sign_extension(op0, width);
   }
 
   return SUB::convert_bitvector(expr);
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 752fe9fab3c..f8f0c151119 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -3425,11 +3425,17 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
         convert_expr(src);
       else if(from_width<to_width)
       {
-        out << "((_ sign_extend "
-            << (to_width-from_width)
-            << ") ";
+        // Extend according to the signedness of the source type (GCC
+        // semantics for implementation-defined integer-to-pointer
+        // conversion).
+        if(src_type.id() == ID_signedbv)
+          out << "((_ sign_extend ";
+        else
+          out << "((_ zero_extend ";
+
+        out << (to_width - from_width) << ") ";
         convert_expr(src);
-        out << ")"; // sign_extend
+        out << ")";
       }
       else // from_width>to_width
       {