diff --git a/regression/cbmc/union13/no-arch.desc b/regression/cbmc/union13/no-arch.desc
index 1e796102550..b43b43ef367 100644
--- a/regression/cbmc/union13/no-arch.desc
+++ b/regression/cbmc/union13/no-arch.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --arch none --little-endian
 (Starting CEGAR Loop|^Generated 1 VCC\(s\), 1 remaining after simplification$)
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index bbfc6d498f0..d7806a971b3 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -3318,8 +3318,14 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
           << ")";
     }
     else
-      UNEXPECTEDCASE(
-        "unknown pointer constant: " + id2string(expr.get_value()));
+    {
+      // just treat the pointer as a bit vector
+      const std::size_t width = boolbv_width(expr_type);
+
+      const mp_integer value = bvrep2integer(expr.get_value(), width, false);
+
+      out << "(_ bv" << value << " " << width << ")";
+    }
   }
   else if(expr_type.id()==ID_bool)
   {