diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc
index 77c4e0af53a..12560af6f29 100644
--- a/regression/cbmc/memory_allocation1/test.desc
+++ b/regression/cbmc/memory_allocation1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/trace-values/unbounded_array.c b/regression/cbmc/trace-values/unbounded_array.c
new file mode 100644
index 00000000000..2f9ced0fdf6
--- /dev/null
+++ b/regression/cbmc/trace-values/unbounded_array.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main(int argc, char *argv[])
+{
+  unsigned long size;
+  __CPROVER_assume(size < 100 && size > 10);
+  int *array = malloc(size * sizeof(int));
+  array[size - 1] = 42;
+  int fixed_array[] = {1, 2};
+  __CPROVER_array_replace(array, fixed_array);
+  assert(array[0] == 0);
+}
diff --git a/regression/cbmc/trace-values/unbounded_array.desc b/regression/cbmc/trace-values/unbounded_array.desc
new file mode 100644
index 00000000000..3fd8d3b3c16
--- /dev/null
+++ b/regression/cbmc/trace-values/unbounded_array.desc
@@ -0,0 +1,13 @@
+CORE broken-smt-backend
+unbounded_array.c
+--trace
+\{ \[0u?l?l?\]=1, \[1u?l?l?\]=2, \[\d+u?l?l?\]=42 \}
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+We generated output like { 1, 2, *, *, *, *, *, *, *, *, *, *, *, 42 } for
+arrays below a certain bound (100 elements), or possibly also empty arrays if
+the size wasn't fixed.
diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc
index 82b3a34754a..d568171b1a6 100644
--- a/regression/cbmc/union12/test.desc
+++ b/regression/cbmc/union12/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index 38fd399791c..67995bc80c7 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -226,6 +226,7 @@ class boolbvt:public arrayst
   virtual exprt bv_get_unbounded_array(const exprt &) const;
 
   virtual exprt bv_get_rec(
+    const exprt &expr,
     const bvt &bv,
     const std::vector<bool> &unknown,
     std::size_t offset,
diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp
index a307d258c4c..94996d45e2d 100644
--- a/src/solvers/flattening/boolbv_get.cpp
+++ b/src/solvers/flattening/boolbv_get.cpp
@@ -11,10 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/simplify_expr.h>
 #include <util/std_expr.h>
-#include <util/threeval.h>
 #include <util/std_types.h>
-#include <util/simplify_expr.h>
+#include <util/threeval.h>
 
 #include "boolbv_type.h"
 
@@ -37,9 +38,6 @@ exprt boolbvt::get(const exprt &expr) const
       // the mapping
       PRECONDITION(expr.type() == typet() || expr.type() == map_entry.type);
 
-      if(is_unbounded_array(map_entry.type))
-        return bv_get_unbounded_array(expr);
-
       std::vector<bool> unknown;
       bvt bv;
       std::size_t width=map_entry.width;
@@ -63,7 +61,7 @@ exprt boolbvt::get(const exprt &expr) const
         }
       }
 
-      return bv_get_rec(bv, unknown, 0, map_entry.type);
+      return bv_get_rec(expr, bv, unknown, 0, map_entry.type);
     }
   }
 
@@ -71,6 +69,7 @@ exprt boolbvt::get(const exprt &expr) const
 }
 
 exprt boolbvt::bv_get_rec(
+  const exprt &expr,
   const bvt &bv,
   const std::vector<bool> &unknown,
   std::size_t offset,
@@ -93,7 +92,7 @@ exprt boolbvt::bv_get_rec(
       }
     }
 
-    return nil_exprt();
+    return false_exprt{}; // default
   }
 
   bvtypet bvtype=get_bvtype(type);
@@ -102,6 +101,9 @@ exprt boolbvt::bv_get_rec(
   {
     if(type.id()==ID_array)
     {
+      if(is_unbounded_array(type))
+        return bv_get_unbounded_array(expr);
+
       const typet &subtype=type.subtype();
       std::size_t sub_width=boolbv_width(subtype);
 
@@ -114,8 +116,10 @@ exprt boolbvt::bv_get_rec(
             new_offset<width;
             new_offset+=sub_width)
         {
+          const index_exprt index{
+            expr, from_integer(new_offset / sub_width, index_type())};
           op.push_back(
-            bv_get_rec(bv, unknown, offset+new_offset, subtype));
+            bv_get_rec(index, bv, unknown, offset + new_offset, subtype));
         }
 
         exprt dest=exprt(ID_array, type);
@@ -126,14 +130,14 @@ exprt boolbvt::bv_get_rec(
     else if(type.id()==ID_struct_tag)
     {
       exprt result = bv_get_rec(
-        bv, unknown, offset, ns.follow_tag(to_struct_tag_type(type)));
+        expr, bv, unknown, offset, ns.follow_tag(to_struct_tag_type(type)));
       result.type() = type;
       return result;
     }
     else if(type.id()==ID_union_tag)
     {
-      exprt result =
-        bv_get_rec(bv, unknown, offset, ns.follow_tag(to_union_tag_type(type)));
+      exprt result = bv_get_rec(
+        expr, bv, unknown, offset, ns.follow_tag(to_union_tag_type(type)));
       result.type() = type;
       return result;
     }
@@ -148,15 +152,14 @@ exprt boolbvt::bv_get_rec(
       for(const auto &c : components)
       {
         const typet &subtype = c.type();
-        op.push_back(nil_exprt());
 
-        std::size_t sub_width=boolbv_width(subtype);
+        const member_exprt member{expr, c.get_name(), subtype};
+        op.push_back(
+          bv_get_rec(member, bv, unknown, offset + new_offset, subtype));
 
+        std::size_t sub_width = boolbv_width(subtype);
         if(sub_width!=0)
-        {
-          op.back()=bv_get_rec(bv, unknown, offset+new_offset, subtype);
           new_offset+=sub_width;
-        }
       }
 
       return struct_exprt(std::move(op), type);
@@ -173,9 +176,11 @@ exprt boolbvt::bv_get_rec(
 
       const typet &subtype = components[component_nr].type();
 
+      const member_exprt member{
+        expr, components[component_nr].get_name(), subtype};
       return union_exprt(
         components[component_nr].get_name(),
-        bv_get_rec(bv, unknown, offset, subtype),
+        bv_get_rec(member, bv, unknown, offset, subtype),
         union_type);
     }
     else if(type.id()==ID_vector)
@@ -190,8 +195,11 @@ exprt boolbvt::bv_get_rec(
         value.reserve_operands(size);
 
         for(std::size_t i=0; i<size; i++)
+        {
+          const index_exprt index{expr, from_integer(i, index_type())};
           value.operands().push_back(
-            bv_get_rec(bv, unknown, i*sub_width, subtype));
+            bv_get_rec(index, bv, unknown, i * sub_width, subtype));
+        }
 
         return std::move(value);
       }
@@ -204,8 +212,10 @@ exprt boolbvt::bv_get_rec(
       if(sub_width!=0 && width==sub_width*2)
       {
         const complex_exprt value(
-          bv_get_rec(bv, unknown, 0 * sub_width, subtype),
-          bv_get_rec(bv, unknown, 1 * sub_width, subtype),
+          bv_get_rec(
+            complex_real_exprt{expr}, bv, unknown, 0 * sub_width, subtype),
+          bv_get_rec(
+            complex_imag_exprt{expr}, bv, unknown, 1 * sub_width, subtype),
           to_complex_type(type));
 
         return value;
@@ -236,6 +246,7 @@ exprt boolbvt::bv_get_rec(
   switch(bvtype)
   {
   case bvtypet::IS_UNKNOWN:
+    PRECONDITION(type.id() == ID_string || type.id() == ID_empty);
     if(type.id()==ID_string)
     {
       mp_integer int_value=binary2integer(value, false);
@@ -247,6 +258,10 @@ exprt boolbvt::bv_get_rec(
 
       return constant_exprt(s, type);
     }
+    else if(type.id() == ID_empty)
+    {
+      return constant_exprt{irep_idt(), type};
+    }
     break;
 
   case bvtypet::IS_RANGE:
@@ -267,14 +282,14 @@ exprt boolbvt::bv_get_rec(
   }
   }
 
-  return nil_exprt();
+  UNREACHABLE;
 }
 
 exprt boolbvt::bv_get(const bvt &bv, const typet &type) const
 {
   std::vector<bool> unknown;
   unknown.resize(bv.size(), false);
-  return bv_get_rec(bv, unknown, 0, type);
+  return bv_get_rec(nil_exprt{}, bv, unknown, 0, type);
 }
 
 exprt boolbvt::bv_get_cache(const exprt &expr) const
@@ -284,8 +299,7 @@ exprt boolbvt::bv_get_cache(const exprt &expr) const
 
   // look up literals in cache
   bv_cachet::const_iterator it=bv_cache.find(expr);
-  if(it==bv_cache.end())
-    return nil_exprt();
+  CHECK_RETURN(it != bv_cache.end());
 
   return bv_get(it->second, expr.type());
 }
@@ -298,36 +312,24 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
   const exprt &size_expr=to_array_type(type).size();
   exprt size=simplify_expr(get(size_expr), ns);
 
-  // no size, give up
-  if(size.is_nil())
-    return nil_exprt();
-
   // get the numeric value, unless it's infinity
-  mp_integer size_mpint;
+  mp_integer size_mpint = 0;
 
-  if(size.id()!=ID_infinity)
+  if(size.is_not_nil() && size.id() != ID_infinity)
   {
     const auto size_opt = numeric_cast<mp_integer>(size);
-    if(!size_opt.has_value() || *size_opt < 0)
-      return nil_exprt();
-    else
+    if(size_opt.has_value() && *size_opt >= 0)
       size_mpint = *size_opt;
   }
-  else
-    size_mpint=0;
 
   // search array indices
 
   typedef std::map<mp_integer, exprt> valuest;
   valuest values;
 
+  const auto opt_num = arrays.get_number(expr);
+  if(opt_num.has_value())
   {
-    const auto opt_num = arrays.get_number(expr);
-    if(!opt_num)
-    {
-      return nil_exprt();
-    }
-
     // get root
     const auto number = arrays.find_number(*opt_num);
 
@@ -363,10 +365,9 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
 
   exprt result;
 
-  if(size_mpint>100 || size.id()==ID_infinity)
+  if(values.size() != size_mpint)
   {
     result = array_list_exprt({}, to_array_type(type));
-    result.type().set(ID_size, integer2string(size_mpint));
 
     result.operands().reserve(values.size()*2);
 
@@ -382,15 +383,10 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
   {
     // set the size
     result=exprt(ID_array, type);
-    result.type().set(ID_size, size);
-
-    std::size_t size_int = numeric_cast_v<std::size_t>(size_mpint);
 
     // allocate operands
-    result.operands().resize(size_int);
-
-    for(std::size_t i=0; i<size_int; i++)
-      result.operands()[i]=exprt(ID_unknown);
+    std::size_t size_int = numeric_cast_v<std::size_t>(size_mpint);
+    result.operands().resize(size_int, exprt{ID_unknown});
 
     // search uninterpreted functions
 
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 6a61d2fa345..35f65a474a5 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -585,13 +585,14 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
 }
 
 exprt bv_pointerst::bv_get_rec(
+  const exprt &expr,
   const bvt &bv,
   const std::vector<bool> &unknown,
   std::size_t offset,
   const typet &type) const
 {
   if(type.id()!=ID_pointer)
-    return SUB::bv_get_rec(bv, unknown, offset, type);
+    return SUB::bv_get_rec(expr, bv, unknown, offset, type);
 
   std::string value_addr, value_offset, value;
 
diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h
index a6c7633702f..8a1a8df97de 100644
--- a/src/solvers/flattening/bv_pointers.h
+++ b/src/solvers/flattening/bv_pointers.h
@@ -43,6 +43,7 @@ class bv_pointerst:public boolbvt
   bvt convert_bitvector(const exprt &expr) override; // no cache
 
   exprt bv_get_rec(
+    const exprt &expr,
     const bvt &bv,
     const std::vector<bool> &unknown,
     std::size_t offset,