diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index e2d0662981d..e5df07a7f10 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -128,7 +128,6 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_unary_minus.cpp \
       flattening/boolbv_union.cpp \
       flattening/boolbv_update.cpp \
-      flattening/boolbv_vector.cpp \
       flattening/boolbv_width.cpp \
       flattening/boolbv_with.cpp \
       flattening/bv_dimacs.cpp \
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 68b401d7ee7..1ee94ac9f54 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -192,8 +192,6 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   }
   else if(expr.id()==ID_array)
     return convert_array(expr);
-  else if(expr.id()==ID_vector)
-    return convert_vector(to_vector_expr(expr));
   else if(expr.id()==ID_complex)
     return convert_complex(to_complex_expr(expr));
   else if(expr.id()==ID_complex_real)
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index 1636dd67ffa..882a3eb1f8f 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -157,7 +157,6 @@ class boolbvt:public arrayst
   virtual bvt convert_if(const if_exprt &expr);
   virtual bvt convert_struct(const struct_exprt &expr);
   virtual bvt convert_array(const exprt &expr);
-  virtual bvt convert_vector(const vector_exprt &expr);
   virtual bvt convert_complex(const complex_exprt &expr);
   virtual bvt convert_complex_real(const complex_real_exprt &expr);
   virtual bvt convert_complex_imag(const complex_imag_exprt &expr);
diff --git a/src/solvers/flattening/boolbv_add_sub.cpp b/src/solvers/flattening/boolbv_add_sub.cpp
index 59d245d72da..72c1e93bebe 100644
--- a/src/solvers/flattening/boolbv_add_sub.cpp
+++ b/src/solvers/flattening/boolbv_add_sub.cpp
@@ -21,14 +21,13 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
   const typet &type = expr.type();
 
-  if(type.id()!=ID_unsignedbv &&
-     type.id()!=ID_signedbv &&
-     type.id()!=ID_fixedbv &&
-     type.id()!=ID_floatbv &&
-     type.id()!=ID_range &&
-     type.id()!=ID_complex &&
-     type.id()!=ID_vector)
+  if(
+    type.id() != ID_unsignedbv && type.id() != ID_signedbv &&
+    type.id() != ID_fixedbv && type.id() != ID_floatbv &&
+    type.id() != ID_range && type.id() != ID_complex)
+  {
     return conversion_failed(expr);
+  }
 
   std::size_t width=boolbv_width(type);
 
@@ -50,9 +49,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
   bool no_overflow=(expr.id()=="no-overflow-plus" ||
                     expr.id()=="no-overflow-minus");
 
-  typet arithmetic_type = (type.id() == ID_vector || type.id() == ID_complex)
-                            ? to_type_with_subtype(type).subtype()
-                            : type;
+  typet arithmetic_type =
+    type.id() == ID_complex ? to_type_with_subtype(type).subtype() : type;
 
   bv_utilst::representationt rep=
     (arithmetic_type.id()==ID_signedbv ||
@@ -68,15 +66,16 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
     const bvt &op = convert_bv(*it, width);
 
-    if(type.id()==ID_vector || type.id()==ID_complex)
+    if(type.id() == ID_complex)
     {
       std::size_t sub_width =
         boolbv_width(to_type_with_subtype(type).subtype());
 
-      INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
+      INVARIANT(
+        sub_width != 0, "complex elements shall have nonzero bit width");
       INVARIANT(
         width % sub_width == 0,
-        "total vector bit width shall be a multiple of the element bit width");
+        "total complex bit width shall be a multiple of the element bit width");
 
       std::size_t size=width/sub_width;
       bv.resize(width);
@@ -149,8 +148,7 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
 
   if(
     type.id() != ID_unsignedbv && type.id() != ID_signedbv &&
-    type.id() != ID_fixedbv && type.id() != ID_complex &&
-    type.id() != ID_vector)
+    type.id() != ID_fixedbv && type.id() != ID_complex)
   {
     return conversion_failed(expr);
   }
@@ -163,9 +161,8 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
 
   const bool subtract = expr.id() == ID_saturating_minus;
 
-  typet arithmetic_type = (type.id() == ID_vector || type.id() == ID_complex)
-                            ? to_type_with_subtype(type).subtype()
-                            : type;
+  typet arithmetic_type =
+    type.id() == ID_complex ? to_type_with_subtype(type).subtype() : type;
 
   bv_utilst::representationt rep =
     (arithmetic_type.id() == ID_signedbv || arithmetic_type.id() == ID_fixedbv)
@@ -175,15 +172,15 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
   bvt bv = convert_bv(expr.lhs(), width);
   const bvt &op = convert_bv(expr.rhs(), width);
 
-  if(type.id() != ID_vector && type.id() != ID_complex)
+  if(type.id() != ID_complex)
     return bv_utils.saturating_add_sub(bv, op, subtract, rep);
 
   std::size_t sub_width = boolbv_width(to_type_with_subtype(type).subtype());
 
-  INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
+  INVARIANT(sub_width != 0, "complex elements shall have nonzero bit width");
   INVARIANT(
     width % sub_width == 0,
-    "total vector bit width shall be a multiple of the element bit width");
+    "total complex bit width shall be a multiple of the element bit width");
 
   std::size_t size = width / sub_width;
 
diff --git a/src/solvers/flattening/boolbv_floatbv_op.cpp b/src/solvers/flattening/boolbv_floatbv_op.cpp
index b3909dac0d7..e42479573f5 100644
--- a/src/solvers/flattening/boolbv_floatbv_op.cpp
+++ b/src/solvers/flattening/boolbv_floatbv_op.cpp
@@ -116,7 +116,7 @@ bvt boolbvt::convert_floatbv_op(const ieee_float_op_exprt &expr)
     else
       UNREACHABLE;
   }
-  else if(expr.type().id() == ID_vector || expr.type().id() == ID_complex)
+  else if(expr.type().id() == ID_complex)
   {
     const typet &subtype = to_type_with_subtype(expr.type()).subtype();
 
@@ -129,8 +129,8 @@ bvt boolbvt::convert_floatbv_op(const ieee_float_op_exprt &expr)
 
       DATA_INVARIANT(
         sub_width > 0 && width % sub_width == 0,
-        "width of a vector subtype must be positive and evenly divide the "
-        "width of the vector");
+        "width of a complex subtype must be positive and evenly divide the "
+        "width of the complex expression");
 
       std::size_t size=width/sub_width;
       bvt result_bv;
@@ -160,7 +160,7 @@ bvt boolbvt::convert_floatbv_op(const ieee_float_op_exprt &expr)
 
         INVARIANT(
           sub_result_bv.size() == sub_width,
-          "we constructed a new vector of the right size");
+          "we constructed a new complex of the right size");
         INVARIANT(
           i * sub_width + sub_width - 1 < result_bv.size(),
           "the sub-bitvector fits into the result bitvector");
diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp
index ca38d78a5f6..25377dde955 100644
--- a/src/solvers/flattening/boolbv_get.cpp
+++ b/src/solvers/flattening/boolbv_get.cpp
@@ -153,31 +153,6 @@ exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset)
         bv_get_rec(member, bv, offset),
         type);
     }
-    else if(type.id()==ID_vector)
-    {
-      const std::size_t width = boolbv_width(type);
-
-      const auto &vector_type = to_vector_type(type);
-      const typet &element_type = vector_type.element_type();
-      std::size_t element_width = boolbv_width(element_type);
-      CHECK_RETURN(element_width > 0);
-
-      if(element_width != 0 && width % element_width == 0)
-      {
-        std::size_t size = width / element_width;
-        vector_exprt value({}, vector_type);
-        value.reserve_operands(size);
-
-        for(std::size_t i=0; i<size; i++)
-        {
-          const index_exprt index{expr,
-                                  from_integer(i, vector_type.index_type())};
-          value.operands().push_back(bv_get_rec(index, bv, i * element_width));
-        }
-
-        return std::move(value);
-      }
-    }
     else if(type.id()==ID_complex)
     {
       const std::size_t width = boolbv_width(type);
diff --git a/src/solvers/flattening/boolbv_unary_minus.cpp b/src/solvers/flattening/boolbv_unary_minus.cpp
index ad7924adc5f..5df1699c7a4 100644
--- a/src/solvers/flattening/boolbv_unary_minus.cpp
+++ b/src/solvers/flattening/boolbv_unary_minus.cpp
@@ -30,8 +30,7 @@ bvt boolbvt::convert_unary_minus(const unary_minus_exprt &expr)
   bvtypet bvtype=get_bvtype(type);
   bvtypet op_bvtype = get_bvtype(op.type());
 
-  if(bvtype==bvtypet::IS_UNKNOWN &&
-     (type.id()==ID_vector || type.id()==ID_complex))
+  if(bvtype == bvtypet::IS_UNKNOWN && type.id() == ID_complex)
   {
     const typet &subtype = to_type_with_subtype(type).subtype();
 
diff --git a/src/solvers/flattening/boolbv_vector.cpp b/src/solvers/flattening/boolbv_vector.cpp
deleted file mode 100644
index 507f858824d..00000000000
--- a/src/solvers/flattening/boolbv_vector.cpp
+++ /dev/null
@@ -1,34 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-
-#include "boolbv.h"
-
-bvt boolbvt::convert_vector(const vector_exprt &expr)
-{
-  std::size_t width=boolbv_width(expr.type());
-
-  const exprt::operandst &operands = expr.operands();
-
-  bvt bv;
-  bv.reserve(width);
-
-  if(!operands.empty())
-  {
-    std::size_t op_width = width / operands.size();
-
-    for(const auto &op : operands)
-    {
-      const bvt &tmp = convert_bv(op, op_width);
-
-      bv.insert(bv.end(), tmp.begin(), tmp.end());
-    }
-  }
-
-  return bv;
-}
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index 1be31bf350a..41885c469c8 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/src/solvers/flattening/boolbv_width.cpp
@@ -149,21 +149,6 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     else
       cache_entry = defined_entryt{numeric_cast_v<std::size_t>(total)};
   }
-  else if(type_id==ID_vector)
-  {
-    const vector_typet &vector_type=to_vector_type(type);
-    auto sub_width = get_width_opt(vector_type.element_type());
-    if(!sub_width.has_value())
-      return cache_entry;
-
-    const auto vector_size = numeric_cast_v<mp_integer>(vector_type.size());
-
-    mp_integer total = vector_size * *sub_width;
-    if(total > (1 << 30)) // realistic limit
-      throw analysis_exceptiont("vector too large for flattening");
-    else
-      cache_entry = defined_entryt{numeric_cast_v<std::size_t>(total)};
-  }
   else if(type_id==ID_complex)
   {
     auto sub_width = get_width_opt(to_complex_type(type).subtype());
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index b4312756dec..4e4e7ac6c88 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -1246,43 +1246,9 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     const bitnot_exprt &bitnot_expr = to_bitnot_expr(expr);
 
-    if(bitnot_expr.type().id() == ID_vector)
-    {
-      if(use_datatypes)
-      {
-        const std::string &smt_typename = datatype_map.at(bitnot_expr.type());
-
-        // extract elements
-        const vector_typet &vector_type = to_vector_type(bitnot_expr.type());
-
-        mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
-
-        out << "(let ((?vectorop ";
-        convert_expr(bitnot_expr.op());
-        out << ")) ";
-
-        out << "(mk-" << smt_typename;
-
-        typet index_type=vector_type.size().type();
-
-        // do bitnot component-by-component
-        for(mp_integer i=0; i!=size; ++i)
-        {
-          out << " (bvnot (" << smt_typename << "." << (size-i-1)
-              << " ?vectorop))";
-        }
-
-        out << "))"; // mk-, let
-      }
-      else
-        SMT2_TODO("bitnot for vectors");
-    }
-    else
-    {
-      out << "(bvnot ";
-      convert_expr(bitnot_expr.op());
-      out << ")";
-    }
+    out << "(bvnot ";
+    convert_expr(bitnot_expr.op());
+    out << ")";
   }
   else if(expr.id()==ID_unary_minus)
   {
@@ -1309,39 +1275,6 @@ void smt2_convt::convert_expr(const exprt &expr)
       else
         convert_floatbv(unary_minus_expr);
     }
-    else if(unary_minus_expr.type().id() == ID_vector)
-    {
-      if(use_datatypes)
-      {
-        const std::string &smt_typename =
-          datatype_map.at(unary_minus_expr.type());
-
-        // extract elements
-        const vector_typet &vector_type =
-          to_vector_type(unary_minus_expr.type());
-
-        mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
-
-        out << "(let ((?vectorop ";
-        convert_expr(unary_minus_expr.op());
-        out << ")) ";
-
-        out << "(mk-" << smt_typename;
-
-        typet index_type=vector_type.size().type();
-
-        // negate component-by-component
-        for(mp_integer i=0; i!=size; ++i)
-        {
-          out << " (bvneg (" << smt_typename << "." << (size-i-1)
-              << " ?vectorop))";
-        }
-
-        out << "))"; // mk-, let
-      }
-      else
-        SMT2_TODO("unary minus for vector");
-    }
     else
     {
       out << "(bvneg ";
@@ -2386,35 +2319,6 @@ void smt2_convt::convert_expr(const exprt &expr)
 
     out << ')';
   }
-  else if(expr.id()==ID_vector)
-  {
-    const vector_exprt &vector_expr = to_vector_expr(expr);
-    const vector_typet &vector_type = to_vector_type(vector_expr.type());
-
-    mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
-
-    DATA_INVARIANT(
-      size == vector_expr.operands().size(),
-      "size indicated by type shall be equal to the number of operands");
-
-    if(use_datatypes)
-    {
-      const std::string &smt_typename = datatype_map.at(vector_type);
-
-      out << "(mk-" << smt_typename;
-    }
-    else
-      out << "(concat";
-
-    // build component-by-component
-    for(const auto &op : vector_expr.operands())
-    {
-      out << " ";
-      convert_expr(op);
-    }
-
-    out << ")"; // mk-... or concat
-  }
   else if(
     const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
   {
@@ -3801,42 +3705,6 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
       convert_plus(to_plus_expr(make_binary(expr)));
     }
   }
-  else if(expr.type().id() == ID_vector)
-  {
-    const vector_typet &vector_type = to_vector_type(expr.type());
-
-    mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
-
-    typet index_type = vector_type.size().type();
-
-    if(use_datatypes)
-    {
-      const std::string &smt_typename = datatype_map.at(vector_type);
-
-      out << "(mk-" << smt_typename;
-    }
-    else
-      out << "(concat";
-
-    // add component-by-component
-    for(mp_integer i = 0; i != size; ++i)
-    {
-      exprt::operandst summands;
-      summands.reserve(expr.operands().size());
-      for(const auto &op : expr.operands())
-        summands.push_back(index_exprt(
-          op,
-          from_integer(size - i - 1, index_type),
-          vector_type.element_type()));
-
-      plus_exprt tmp(std::move(summands), vector_type.element_type());
-
-      out << " ";
-      convert_expr(tmp);
-    }
-
-    out << ")"; // mk-... or concat
-  }
   else
     UNEXPECTEDCASE("unsupported type for +: " + expr.type().id_string());
 }
@@ -3908,9 +3776,7 @@ void smt2_convt::convert_floatbv_plus(const ieee_float_op_exprt &expr)
   PRECONDITION(
     type.id() == ID_floatbv ||
     (type.id() == ID_complex &&
-     to_complex_type(type).subtype().id() == ID_floatbv) ||
-    (type.id() == ID_vector &&
-     to_vector_type(type).element_type().id() == ID_floatbv));
+     to_complex_type(type).subtype().id() == ID_floatbv));
 
   if(use_FPA_theory)
   {
@@ -3928,10 +3794,6 @@ void smt2_convt::convert_floatbv_plus(const ieee_float_op_exprt &expr)
     {
       SMT2_TODO("+ for floatbv complex");
     }
-    else if(type.id()==ID_vector)
-    {
-      SMT2_TODO("+ for floatbv vector");
-    }
     else
       INVARIANT_WITH_DIAGNOSTICS(
         false,
@@ -4017,41 +3879,6 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
         "unsupported operand types for -: " + expr.op0().type().id_string() +
         " and " + expr.op1().type().id_string());
   }
-  else if(expr.type().id()==ID_vector)
-  {
-    const vector_typet &vector_type=to_vector_type(expr.type());
-
-    mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
-
-    typet index_type=vector_type.size().type();
-
-    if(use_datatypes)
-    {
-      const std::string &smt_typename = datatype_map.at(vector_type);
-
-      out << "(mk-" << smt_typename;
-    }
-    else
-      out << "(concat";
-
-    // subtract component-by-component
-    for(mp_integer i=0; i!=size; ++i)
-    {
-      exprt tmp(ID_minus, vector_type.element_type());
-      for(const auto &op : expr.operands())
-      {
-        tmp.copy_to_operands(index_exprt(
-          op,
-          from_integer(size - i - 1, index_type),
-          vector_type.element_type()));
-      }
-
-      out << " ";
-      convert_expr(tmp);
-    }
-
-    out << ")"; // mk-... or concat
-  }
   else
     UNEXPECTEDCASE("unsupported type for -: "+expr.type().id_string());
 }
@@ -4568,33 +4395,6 @@ void smt2_convt::convert_index(const index_exprt &expr)
       unflatten(wheret::END, array_type.element_type());
     }
   }
-  else if(array_op_type.id()==ID_vector)
-  {
-    const vector_typet &vector_type=to_vector_type(array_op_type);
-
-    if(use_datatypes)
-    {
-      const std::string &smt_typename = datatype_map.at(vector_type);
-
-      // this is easy for constant indicies
-
-      const auto index_int = numeric_cast<mp_integer>(expr.index());
-      if(!index_int.has_value())
-      {
-        SMT2_TODO("non-constant index on vectors");
-      }
-      else
-      {
-        out << "(" << smt_typename << "." << *index_int << " ";
-        convert_expr(expr.array());
-        out << ")";
-      }
-    }
-    else
-    {
-      SMT2_TODO("index on vectors");
-    }
-  }
   else
     INVARIANT(
       false, "index with unsupported array type: " + array_op_type.id_string());
@@ -4671,33 +4471,6 @@ void smt2_convt::flatten2bv(const exprt &expr)
     convert_expr(expr); // this returns a Bool
     out << " #b1 #b0)"; // this is a one-bit bit-vector
   }
-  else if(type.id()==ID_vector)
-  {
-    if(use_datatypes)
-    {
-      const std::string &smt_typename = datatype_map.at(type);
-
-      // concatenate elements
-      const vector_typet &vector_type=to_vector_type(type);
-
-      mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
-
-      out << "(let ((?vflop ";
-      convert_expr(expr);
-      out << ")) ";
-
-      out << "(concat";
-
-      for(mp_integer i=0; i!=size; ++i)
-      {
-        out << " (" << smt_typename << "." << i << " ?vflop)";
-      }
-
-      out << "))"; // concat, let
-    }
-    else
-      convert_expr(expr); // already a bv
-  }
   else if(type.id()==ID_array)
   {
     if(use_array_theory(expr))
@@ -4789,46 +4562,6 @@ void smt2_convt::unflatten(
     else
       out << " #b1)";
   }
-  else if(type.id()==ID_vector)
-  {
-    if(use_datatypes)
-    {
-      const std::string &smt_typename = datatype_map.at(type);
-
-      // extract elements
-      const vector_typet &vector_type=to_vector_type(type);
-
-      std::size_t subtype_width = boolbv_width(vector_type.element_type());
-
-      mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
-
-      if(where==wheret::BEGIN)
-        out << "(let ((?ufop" << nesting << " ";
-      else
-      {
-        out << ")) ";
-
-        out << "(mk-" << smt_typename;
-
-        std::size_t offset=0;
-
-        for(mp_integer i=0; i!=size; ++i, offset+=subtype_width)
-        {
-          out << " ";
-          unflatten(wheret::BEGIN, vector_type.element_type(), nesting + 1);
-          out << "((_ extract " << offset+subtype_width-1 << " "
-              << offset << ") ?ufop" << nesting << ")";
-          unflatten(wheret::END, vector_type.element_type(), nesting + 1);
-        }
-
-        out << "))"; // mk-, let
-      }
-    }
-    else
-    {
-      // nop, already a bv
-    }
-  }
   else if(type.id() == ID_array)
   {
     if(use_datatypes)
@@ -5744,19 +5477,6 @@ void smt2_convt::convert_type(const typet &type)
       out << "(_ BitVec " << width << ")";
     }
   }
-  else if(type.id()==ID_vector)
-  {
-    if(use_datatypes)
-    {
-      out << datatype_map.at(type);
-    }
-    else
-    {
-      std::size_t width=boolbv_width(type);
-
-      out << "(_ BitVec " << width << ")";
-    }
-  }
   else if(type.id()==ID_code)
   {
     // These may appear in structs.
@@ -5883,34 +5603,6 @@ void smt2_convt::find_symbols_rec(
       out << "))))\n";
     }
   }
-  else if(type.id()==ID_vector)
-  {
-    find_symbols_rec(to_vector_type(type).element_type(), recstack);
-
-    if(use_datatypes &&
-       datatype_map.find(type)==datatype_map.end())
-    {
-      const vector_typet &vector_type=to_vector_type(type);
-
-      mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
-
-      const std::string smt_typename =
-        "vector." + std::to_string(datatype_map.size());
-      datatype_map[type] = smt_typename;
-
-      out << "(declare-datatypes ((" << smt_typename << " 0)) "
-          << "(((mk-" << smt_typename;
-
-      for(mp_integer i=0; i!=size; ++i)
-      {
-        out << " (" << smt_typename << "." << i << " ";
-        convert_type(to_vector_type(type).element_type());
-        out << ")";
-      }
-
-      out << "))))\n";
-    }
-  }
   else if(type.id() == ID_struct)
   {
     // Cater for mutually recursive struct types