diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp b/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp
index c529bf82d37..c16ef865fe4 100644
--- a/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp
+++ b/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp
@@ -4,6 +4,53 @@
 
 #include <util/invariant.h>
 
+const char *smt_bit_vector_theoryt::concatt::identifier()
+{
+  return "concat";
+}
+
+smt_sortt smt_bit_vector_theoryt::concatt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  const auto get_width = [](const smt_termt &term) {
+    return term.get_sort().cast<smt_bit_vector_sortt>()->bit_width();
+  };
+  return smt_bit_vector_sortt{get_width(lhs) + get_width(rhs)};
+}
+
+static void validate_bit_vector_sort(
+  const std::string &descriptor,
+  const smt_termt &operand)
+{
+  const auto operand_sort = operand.get_sort().cast<smt_bit_vector_sortt>();
+  INVARIANT(
+    operand_sort,
+    descriptor + " operand is expected to have a bit-vector sort.");
+}
+
+static void validate_bit_vector_sort(const smt_termt &operand)
+{
+  validate_bit_vector_sort("The", operand);
+}
+
+static void
+validate_bit_vector_sorts(const smt_termt &lhs, const smt_termt &rhs)
+{
+  validate_bit_vector_sort("Left", lhs);
+  validate_bit_vector_sort("Right", rhs);
+}
+
+void smt_bit_vector_theoryt::concatt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_sorts(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::concatt>
+  smt_bit_vector_theoryt::concat{};
+
 const char *smt_bit_vector_theoryt::extractt::identifier()
 {
   return "extract";
@@ -35,21 +82,169 @@ smt_bit_vector_theoryt::extract(std::size_t i, std::size_t j)
   return smt_function_application_termt::factoryt<extractt>(i, j);
 }
 
-static void validate_bit_vector_operator_arguments(
-  const smt_termt &left,
-  const smt_termt &right)
+static void
+validate_matched_bit_vector_sorts(const smt_termt &left, const smt_termt &right)
 {
-  const auto left_sort = left.get_sort().cast<smt_bit_vector_sortt>();
-  INVARIANT(left_sort, "Left operand must have bitvector sort.");
-  const auto right_sort = right.get_sort().cast<smt_bit_vector_sortt>();
-  INVARIANT(right_sort, "Right operand must have bitvector sort.");
+  validate_bit_vector_sorts(left, right);
   // The below invariant is based on the smtlib standard.
   // See http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV
   INVARIANT(
-    left_sort->bit_width() == right_sort->bit_width(),
+    left.get_sort() == right.get_sort(),
     "Left and right operands must have the same bit width.");
 }
 
+// Bitwise operator definitions
+
+const char *smt_bit_vector_theoryt::nott::identifier()
+{
+  return "bvnot";
+}
+
+smt_sortt smt_bit_vector_theoryt::nott::return_sort(const smt_termt &operand)
+{
+  return operand.get_sort();
+}
+
+void smt_bit_vector_theoryt::nott::validate(const smt_termt &operand)
+{
+  validate_bit_vector_sort(operand);
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nott>
+  smt_bit_vector_theoryt::make_not{};
+
+const char *smt_bit_vector_theoryt::andt::identifier()
+{
+  return "bvand";
+}
+
+smt_sortt smt_bit_vector_theoryt::andt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::andt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_matched_bit_vector_sorts(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::andt>
+  smt_bit_vector_theoryt::make_and{};
+
+const char *smt_bit_vector_theoryt::ort::identifier()
+{
+  return "bvor";
+}
+
+smt_sortt smt_bit_vector_theoryt::ort::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::ort::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_matched_bit_vector_sorts(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::ort>
+  smt_bit_vector_theoryt::make_or{};
+
+const char *smt_bit_vector_theoryt::nandt::identifier()
+{
+  return "bvnand";
+}
+
+smt_sortt smt_bit_vector_theoryt::nandt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::nandt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_matched_bit_vector_sorts(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nandt>
+  smt_bit_vector_theoryt::nand{};
+
+const char *smt_bit_vector_theoryt::nort::identifier()
+{
+  return "bvnor";
+}
+
+smt_sortt smt_bit_vector_theoryt::nort::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::nort::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_matched_bit_vector_sorts(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nort>
+  smt_bit_vector_theoryt::nor{};
+
+const char *smt_bit_vector_theoryt::xort::identifier()
+{
+  return "bvxor";
+}
+
+smt_sortt smt_bit_vector_theoryt::xort::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::xort::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_matched_bit_vector_sorts(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::xort>
+  smt_bit_vector_theoryt::make_xor{};
+
+const char *smt_bit_vector_theoryt::xnort::identifier()
+{
+  return "bvxnor";
+}
+
+smt_sortt smt_bit_vector_theoryt::xnort::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::xnort::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_matched_bit_vector_sorts(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::xnort>
+  smt_bit_vector_theoryt::xnor{};
+
 // Relational operator definitions
 
 const char *smt_bit_vector_theoryt::unsigned_less_thant::identifier()
@@ -68,7 +263,7 @@ void smt_bit_vector_theoryt::unsigned_less_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -91,7 +286,7 @@ void smt_bit_vector_theoryt::unsigned_less_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -114,7 +309,7 @@ void smt_bit_vector_theoryt::unsigned_greater_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -138,7 +333,7 @@ void smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -161,7 +356,7 @@ void smt_bit_vector_theoryt::signed_less_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -184,7 +379,7 @@ void smt_bit_vector_theoryt::signed_less_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -207,7 +402,7 @@ void smt_bit_vector_theoryt::signed_greater_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -230,7 +425,7 @@ void smt_bit_vector_theoryt::signed_greater_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -253,7 +448,7 @@ void smt_bit_vector_theoryt::addt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::addt>
@@ -275,7 +470,7 @@ void smt_bit_vector_theoryt::subtractt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -298,7 +493,7 @@ void smt_bit_vector_theoryt::multiplyt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -321,7 +516,7 @@ void smt_bit_vector_theoryt::unsigned_dividet::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -344,7 +539,7 @@ void smt_bit_vector_theoryt::signed_dividet::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -367,7 +562,7 @@ void smt_bit_vector_theoryt::unsigned_remaindert::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -390,7 +585,7 @@ void smt_bit_vector_theoryt::signed_remaindert::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -409,9 +604,77 @@ smt_sortt smt_bit_vector_theoryt::negatet::return_sort(const smt_termt &operand)
 
 void smt_bit_vector_theoryt::negatet::validate(const smt_termt &operand)
 {
-  const auto operand_sort = operand.get_sort().cast<smt_bit_vector_sortt>();
-  INVARIANT(operand_sort, "The operand is expected to have a bit-vector sort.");
+  validate_bit_vector_sort(operand);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::negatet>
   smt_bit_vector_theoryt::negate{};
+
+const char *smt_bit_vector_theoryt::shift_leftt::identifier()
+{
+  return "bvshl";
+}
+
+smt_sortt smt_bit_vector_theoryt::shift_leftt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::shift_leftt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_matched_bit_vector_sorts(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::shift_leftt>
+  smt_bit_vector_theoryt::shift_left{};
+
+const char *smt_bit_vector_theoryt::logical_shift_rightt::identifier()
+{
+  return "bvlshr";
+}
+
+smt_sortt smt_bit_vector_theoryt::logical_shift_rightt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::logical_shift_rightt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_matched_bit_vector_sorts(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::logical_shift_rightt>
+  smt_bit_vector_theoryt::logical_shift_right{};
+
+const char *smt_bit_vector_theoryt::arithmetic_shift_rightt::identifier()
+{
+  return "bvashr";
+}
+
+smt_sortt smt_bit_vector_theoryt::arithmetic_shift_rightt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::arithmetic_shift_rightt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_matched_bit_vector_sorts(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::arithmetic_shift_rightt>
+  smt_bit_vector_theoryt::arithmetic_shift_right{};
diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.h b/src/solvers/smt2_incremental/smt_bit_vector_theory.h
index 07c4b45188a..cfb440d78c9 100644
--- a/src/solvers/smt2_incremental/smt_bit_vector_theory.h
+++ b/src/solvers/smt2_incremental/smt_bit_vector_theory.h
@@ -8,6 +8,14 @@
 class smt_bit_vector_theoryt
 {
 public:
+  struct concatt final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<concatt> concat;
+
   struct extractt final
   {
     std::size_t i;
@@ -20,6 +28,63 @@ class smt_bit_vector_theoryt
   static smt_function_application_termt::factoryt<extractt>
   extract(std::size_t i, std::size_t j);
 
+  // Bitwise operators
+  struct nott final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &operand);
+    static void validate(const smt_termt &operand);
+  };
+  static const smt_function_application_termt::factoryt<nott> make_not;
+
+  struct andt final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<andt> make_and;
+
+  struct ort final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<ort> make_or;
+
+  struct nandt final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<nandt> nand;
+
+  struct nort final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<nort> nor;
+
+  struct xort final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<xort> make_xor;
+
+  struct xnort final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<xnort> xnor;
+
   // Relational operator class declarations
   struct unsigned_less_thant final
   {
@@ -164,6 +229,33 @@ class smt_bit_vector_theoryt
     static void validate(const smt_termt &operand);
   };
   static const smt_function_application_termt::factoryt<negatet> negate;
+
+  // Shift operations
+  struct shift_leftt final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<shift_leftt> shift_left;
+
+  struct logical_shift_rightt final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<logical_shift_rightt>
+    logical_shift_right;
+
+  struct arithmetic_shift_rightt final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<arithmetic_shift_rightt>
+    arithmetic_shift_right;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
diff --git a/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp b/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp
index 8166fe29c36..e663dd30362 100644
--- a/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp
+++ b/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp
@@ -7,6 +7,32 @@
 
 #include <util/mp_arith.h>
 
+TEST_CASE("SMT bit vector concatenation", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt a_valid{42, 8}, b_valid{42, 16};
+  SECTION("Valid operands")
+  {
+    const auto concat = smt_bit_vector_theoryt::concat(a_valid, b_valid);
+    const auto expected_return_sort = smt_bit_vector_sortt{24};
+    REQUIRE(
+      concat.function_identifier() ==
+      smt_identifier_termt("concat", expected_return_sort));
+    REQUIRE(concat.get_sort() == expected_return_sort);
+    REQUIRE(concat.arguments().size() == 2);
+    REQUIRE(concat.arguments()[0].get() == a_valid);
+    REQUIRE(concat.arguments()[1].get() == b_valid);
+  }
+  SECTION("Invalid operands")
+  {
+    const smt_bool_literal_termt false_term{false};
+    const smt_bool_literal_termt true_term{true};
+    cbmc_invariants_should_throwt invariants_throw;
+    CHECK_THROWS(smt_bit_vector_theoryt::concat(a_valid, false_term));
+    CHECK_THROWS(smt_bit_vector_theoryt::concat(false_term, a_valid));
+    CHECK_THROWS(smt_bit_vector_theoryt::concat(false_term, true_term));
+  }
+}
+
 TEST_CASE("SMT bit vector extract", "[core][smt2_incremental]")
 {
   const smt_bit_vector_constant_termt operand{42, 8};
@@ -34,6 +60,120 @@ TEST_CASE("SMT bit vector extract", "[core][smt2_incremental]")
   }
 }
 
+TEST_CASE("SMT bit vector bitwise operators", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt two{2, 8};
+  const smt_bit_vector_constant_termt three{3, 8};
+  const smt_bit_vector_constant_termt wider{4, 16};
+  const smt_bool_literal_termt true_val{true};
+  SECTION("not")
+  {
+    const auto function_application = smt_bit_vector_theoryt::make_not(two);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvnot", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 1);
+    REQUIRE(function_application.arguments()[0].get() == two);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::make_not(true_val));
+  }
+  SECTION("or")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::make_or(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvor", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::make_or(three, wider));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::make_or(true_val, three));
+  }
+  SECTION("and")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::make_and(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvand", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::make_and(three, wider));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::make_and(true_val, three));
+  }
+  SECTION("nand")
+  {
+    const auto function_application = smt_bit_vector_theoryt::nand(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvnand", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::nand(three, wider));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::nand(true_val, three));
+  }
+  SECTION("nor")
+  {
+    const auto function_application = smt_bit_vector_theoryt::nor(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvnor", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::nor(three, wider));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::nor(true_val, three));
+  }
+  SECTION("xor")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::make_xor(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvxor", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::make_xor(three, wider));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::make_xor(true_val, three));
+  }
+  SECTION("xnor")
+  {
+    const auto function_application = smt_bit_vector_theoryt::xnor(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvxnor", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::xnor(three, wider));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::xnor(true_val, three));
+  }
+}
+
 TEST_CASE("SMT bit vector predicates", "[core][smt2_incremental]")
 {
   const smt_bit_vector_constant_termt two{2, 8};
@@ -352,3 +492,62 @@ TEST_CASE(
     REQUIRE_THROWS(smt_bit_vector_theoryt::negate(true_val));
   }
 }
+
+TEST_CASE("SMT bit vector shifts", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt two{2, 8};
+  const smt_bit_vector_constant_termt three{3, 8};
+  const smt_bit_vector_constant_termt wider{4, 16};
+  const smt_bool_literal_termt true_val{true};
+  SECTION("shift left")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::shift_left(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvshl", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::shift_left(three, wider));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::shift_left(true_val, three));
+  }
+  SECTION("logical shift right")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::logical_shift_right(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvlshr", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::logical_shift_right(three, wider));
+    REQUIRE_THROWS(
+      smt_bit_vector_theoryt::logical_shift_right(true_val, three));
+  }
+  SECTION("arithmetic shift right")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::arithmetic_shift_right(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvashr", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(
+      smt_bit_vector_theoryt::arithmetic_shift_right(three, wider));
+    REQUIRE_THROWS(
+      smt_bit_vector_theoryt::arithmetic_shift_right(true_val, three));
+  }
+}