diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
index 6030236f438..07e71c1abca 100644
--- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -154,9 +154,19 @@ static smt_termt convert_expr_to_smt(const bitnot_exprt &bitwise_not)
 
 static smt_termt convert_expr_to_smt(const unary_minus_exprt &unary_minus)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for unary minus expression: " +
-    unary_minus.pretty());
+  const bool operand_is_bitvector =
+    can_cast_type<integer_bitvector_typet>(unary_minus.op().type());
+  if(operand_is_bitvector)
+  {
+    return smt_bit_vector_theoryt::negate(
+      convert_expr_to_smt(unary_minus.op()));
+  }
+  else
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for unary minus expression: " +
+      unary_minus.pretty());
+  }
 }
 
 static smt_termt convert_expr_to_smt(const unary_plus_exprt &unary_plus)
@@ -326,20 +336,67 @@ static optionalt<smt_termt> try_relational_conversion(const exprt &expr)
 
 static smt_termt convert_expr_to_smt(const plus_exprt &plus)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for plus expression: " + plus.pretty());
+  if(std::all_of(
+       plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) {
+         return can_cast_type<integer_bitvector_typet>(operand.type());
+       }))
+  {
+    return convert_multiary_operator_to_terms(
+      plus, smt_bit_vector_theoryt::add);
+  }
+  else
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for plus expression: " + plus.pretty());
+  }
 }
 
 static smt_termt convert_expr_to_smt(const minus_exprt &minus)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for minus expression: " + minus.pretty());
+  const bool both_operands_bitvector =
+    can_cast_type<integer_bitvector_typet>(minus.lhs().type()) &&
+    can_cast_type<integer_bitvector_typet>(minus.rhs().type());
+
+  if(both_operands_bitvector)
+  {
+    return smt_bit_vector_theoryt::subtract(
+      convert_expr_to_smt(minus.lhs()), convert_expr_to_smt(minus.rhs()));
+  }
+  else
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for minus expression: " + minus.pretty());
+  }
 }
 
 static smt_termt convert_expr_to_smt(const div_exprt &divide)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for divide expression: " + divide.pretty());
+  const bool both_operands_bitvector =
+    can_cast_type<integer_bitvector_typet>(divide.lhs().type()) &&
+    can_cast_type<integer_bitvector_typet>(divide.rhs().type());
+
+  const bool both_operands_unsigned =
+    can_cast_type<unsignedbv_typet>(divide.lhs().type()) &&
+    can_cast_type<unsignedbv_typet>(divide.rhs().type());
+
+  if(both_operands_bitvector)
+  {
+    if(both_operands_unsigned)
+    {
+      return smt_bit_vector_theoryt::unsigned_divide(
+        convert_expr_to_smt(divide.lhs()), convert_expr_to_smt(divide.rhs()));
+    }
+    else
+    {
+      return smt_bit_vector_theoryt::signed_divide(
+        convert_expr_to_smt(divide.lhs()), convert_expr_to_smt(divide.rhs()));
+    }
+  }
+  else
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for divide expression: " + divide.pretty());
+  }
 }
 
 static smt_termt convert_expr_to_smt(const ieee_float_op_exprt &float_operation)
@@ -353,9 +410,35 @@ static smt_termt convert_expr_to_smt(const ieee_float_op_exprt &float_operation)
 
 static smt_termt convert_expr_to_smt(const mod_exprt &truncation_modulo)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for truncation modulo expression: " +
-    truncation_modulo.pretty());
+  const bool both_operands_bitvector =
+    can_cast_type<integer_bitvector_typet>(truncation_modulo.lhs().type()) &&
+    can_cast_type<integer_bitvector_typet>(truncation_modulo.rhs().type());
+
+  const bool both_operands_unsigned =
+    can_cast_type<unsignedbv_typet>(truncation_modulo.lhs().type()) &&
+    can_cast_type<unsignedbv_typet>(truncation_modulo.rhs().type());
+
+  if(both_operands_bitvector)
+  {
+    if(both_operands_unsigned)
+    {
+      return smt_bit_vector_theoryt::unsigned_remainder(
+        convert_expr_to_smt(truncation_modulo.lhs()),
+        convert_expr_to_smt(truncation_modulo.rhs()));
+    }
+    else
+    {
+      return smt_bit_vector_theoryt::signed_remainder(
+        convert_expr_to_smt(truncation_modulo.lhs()),
+        convert_expr_to_smt(truncation_modulo.rhs()));
+    }
+  }
+  else
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for remainder (modulus) expression: " +
+      truncation_modulo.pretty());
+  }
 }
 
 static smt_termt
@@ -368,8 +451,22 @@ convert_expr_to_smt(const euclidean_mod_exprt &euclidean_modulo)
 
 static smt_termt convert_expr_to_smt(const mult_exprt &multiply)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for multiply expression: " + multiply.pretty());
+  if(std::all_of(
+       multiply.operands().cbegin(),
+       multiply.operands().cend(),
+       [](exprt operand) {
+         return can_cast_type<integer_bitvector_typet>(operand.type());
+       }))
+  {
+    return convert_multiary_operator_to_terms(
+      multiply, smt_bit_vector_theoryt::multiply);
+  }
+  else
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for multiply expression: " +
+      multiply.pretty());
+  }
 }
 
 static smt_termt convert_expr_to_smt(const address_of_exprt &address_of)
diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp b/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp
index 52641f105a1..50a8a70f677 100644
--- a/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp
+++ b/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp
@@ -4,7 +4,7 @@
 
 #include <util/invariant.h>
 
-static void validate_bit_vector_predicate_arguments(
+static void validate_bit_vector_operator_arguments(
   const smt_termt &left,
   const smt_termt &right)
 {
@@ -37,7 +37,7 @@ void smt_bit_vector_theoryt::unsigned_less_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -60,7 +60,7 @@ void smt_bit_vector_theoryt::unsigned_less_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -83,7 +83,7 @@ void smt_bit_vector_theoryt::unsigned_greater_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -107,7 +107,7 @@ void smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -130,7 +130,7 @@ void smt_bit_vector_theoryt::signed_less_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -153,7 +153,7 @@ void smt_bit_vector_theoryt::signed_less_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -176,7 +176,7 @@ void smt_bit_vector_theoryt::signed_greater_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -199,9 +199,188 @@ void smt_bit_vector_theoryt::signed_greater_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
   smt_bit_vector_theoryt::signed_greater_than_or_equalt>
   smt_bit_vector_theoryt::signed_greater_than_or_equal{};
+
+const char *smt_bit_vector_theoryt::addt::identifier()
+{
+  return "bvadd";
+}
+
+smt_sortt smt_bit_vector_theoryt::addt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::addt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::addt>
+  smt_bit_vector_theoryt::add{};
+
+const char *smt_bit_vector_theoryt::subtractt::identifier()
+{
+  return "bvsub";
+}
+
+smt_sortt smt_bit_vector_theoryt::subtractt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::subtractt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::subtractt>
+  smt_bit_vector_theoryt::subtract{};
+
+const char *smt_bit_vector_theoryt::multiplyt::identifier()
+{
+  return "bvmul";
+}
+
+smt_sortt smt_bit_vector_theoryt::multiplyt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::multiplyt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::multiplyt>
+  smt_bit_vector_theoryt::multiply{};
+
+const char *smt_bit_vector_theoryt::unsigned_dividet::identifier()
+{
+  return "bvudiv";
+}
+
+smt_sortt smt_bit_vector_theoryt::unsigned_dividet::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::unsigned_dividet::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::unsigned_dividet>
+  smt_bit_vector_theoryt::unsigned_divide{};
+
+const char *smt_bit_vector_theoryt::signed_dividet::identifier()
+{
+  return "bvsdiv";
+}
+
+smt_sortt smt_bit_vector_theoryt::signed_dividet::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::signed_dividet::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::signed_dividet>
+  smt_bit_vector_theoryt::signed_divide{};
+
+const char *smt_bit_vector_theoryt::unsigned_remaindert::identifier()
+{
+  return "bvurem";
+}
+
+smt_sortt smt_bit_vector_theoryt::unsigned_remaindert::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::unsigned_remaindert::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::unsigned_remaindert>
+  smt_bit_vector_theoryt::unsigned_remainder{};
+
+const char *smt_bit_vector_theoryt::signed_remaindert::identifier()
+{
+  return "bvsrem";
+}
+
+smt_sortt smt_bit_vector_theoryt::signed_remaindert::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::signed_remaindert::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::signed_remaindert>
+  smt_bit_vector_theoryt::signed_remainder{};
+
+const char *smt_bit_vector_theoryt::negatet::identifier()
+{
+  return "bvneg";
+}
+
+smt_sortt smt_bit_vector_theoryt::negatet::return_sort(const smt_termt &operand)
+{
+  return operand.get_sort();
+}
+
+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.");
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::negatet>
+  smt_bit_vector_theoryt::negate{};
diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.h b/src/solvers/smt2_incremental/smt_bit_vector_theory.h
index 313c900b9bb..b90c5e0ab67 100644
--- a/src/solvers/smt2_incremental/smt_bit_vector_theory.h
+++ b/src/solvers/smt2_incremental/smt_bit_vector_theory.h
@@ -84,6 +84,74 @@ class smt_bit_vector_theoryt
   static const smt_function_application_termt::factoryt<
     signed_greater_than_or_equalt>
     signed_greater_than_or_equal;
+
+  struct addt 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<addt> add;
+
+  struct subtractt 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<subtractt> subtract;
+
+  struct multiplyt 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<multiplyt> multiply;
+
+  struct unsigned_dividet 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<unsigned_dividet>
+    unsigned_divide;
+
+  struct signed_dividet 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<signed_dividet>
+    signed_divide;
+
+  struct unsigned_remaindert 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<unsigned_remaindert>
+    unsigned_remainder;
+
+  struct signed_remaindert 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<signed_remaindert>
+    signed_remainder;
+
+  struct negatet 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<negatet> negate;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp
index 907583764c6..f7939f97da6 100644
--- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -239,3 +239,180 @@ TEST_CASE(
       smt_bit_vector_theoryt::unsigned_less_than_or_equal(one_term, two_term));
   }
 }
+
+TEST_CASE(
+  "expr to smt conversion for arithmetic operators",
+  "[core][smt2_incremental]")
+{
+  const smt_termt smt_term_one = smt_bit_vector_constant_termt{1, 8};
+  const smt_termt smt_term_two = smt_bit_vector_constant_termt{2, 8};
+
+  // Just regular (bit-vector) integers, to be used for the comparison
+  const auto one_bvint = from_integer({1}, signedbv_typet{8});
+  const auto two_bvint = from_integer({2}, signedbv_typet{8});
+  const auto one_bvint_unsigned = from_integer({1}, unsignedbv_typet{8});
+  const auto two_bvint_unsigned = from_integer({2}, unsignedbv_typet{8});
+
+  SECTION("Addition of two constant size bit-vectors")
+  {
+    const auto constructed_term =
+      convert_expr_to_smt(plus_exprt{one_bvint, two_bvint});
+    const auto expected_term =
+      smt_bit_vector_theoryt::add(smt_term_one, smt_term_two);
+    CHECK(constructed_term == expected_term);
+  }
+
+  SECTION(
+    "Addition of four constant size bit-vectors - testing multi-ary handling "
+    "of plus_exprt")
+  {
+    const auto three_bv_int = from_integer({3}, signedbv_typet{8});
+    const auto four_bv_int = from_integer({4}, signedbv_typet{8});
+
+    const auto three_smt_term = smt_bit_vector_constant_termt{3, 8};
+    const auto four_smt_term = smt_bit_vector_constant_termt{4, 8};
+
+    const exprt::operandst plus_operands{
+      one_bvint, two_bvint, three_bv_int, four_bv_int};
+    const auto constructed_term =
+      convert_expr_to_smt(plus_exprt{plus_operands, signedbv_typet{8}});
+    const auto expected_term = smt_bit_vector_theoryt::add(
+      smt_bit_vector_theoryt::add(
+        smt_bit_vector_theoryt::add(smt_term_one, smt_term_two),
+        three_smt_term),
+      four_smt_term);
+
+    CHECK(constructed_term == expected_term);
+  }
+
+  SECTION(
+    "Ensure that addition node conversion fails if the operands are not "
+    "bit-vector based")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(
+      convert_expr_to_smt(plus_exprt{true_exprt{}, false_exprt{}}));
+  }
+
+  SECTION(
+    "Ensure that addition node conversion fails if it has a malformed "
+    "expression")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    // No operands to expression
+    exprt::operandst zero_operands;
+    REQUIRE_THROWS(
+      convert_expr_to_smt(plus_exprt{zero_operands, signedbv_typet{8}}));
+
+    // One operand to expression
+    const auto four_bv_int = from_integer({4}, signedbv_typet{8});
+    exprt::operandst one_operand{four_bv_int};
+    REQUIRE_THROWS(
+      convert_expr_to_smt(plus_exprt{one_operand, signedbv_typet{8}}));
+  }
+
+  SECTION("Subtraction of two constant size bit-vectors")
+  {
+    const auto constructed_term =
+      convert_expr_to_smt(minus_exprt{two_bvint, one_bvint});
+    const auto expected_term =
+      smt_bit_vector_theoryt::subtract(smt_term_two, smt_term_one);
+    CHECK(constructed_term == expected_term);
+  }
+
+  SECTION(
+    "Ensure that subtraction node conversion fails if the operands are not "
+    "bit-vector based")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(
+      convert_expr_to_smt(minus_exprt{true_exprt{}, false_exprt{}}));
+  }
+
+  SECTION("Multiplication of two constant size bit-vectors")
+  {
+    const auto constructed_term =
+      convert_expr_to_smt(mult_exprt{one_bvint, two_bvint});
+    const auto expected_term =
+      smt_bit_vector_theoryt::multiply(smt_term_one, smt_term_two);
+    CHECK(constructed_term == expected_term);
+  }
+
+  SECTION(
+    "Ensure that multiplication node conversion fails if the operands are not "
+    "bit-vector based")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(convert_expr_to_smt(mult_exprt{one_bvint, false_exprt{}}));
+  }
+
+  // Division is defined over unsigned numbers only (theory notes say it
+  // truncates over zero)
+  SECTION("Division of two constant size bit-vectors")
+  {
+    // Check of division expression with unsigned operands
+    const auto constructed_term =
+      convert_expr_to_smt(div_exprt{one_bvint_unsigned, two_bvint_unsigned});
+    const auto expected_term =
+      smt_bit_vector_theoryt::unsigned_divide(smt_term_one, smt_term_two);
+    CHECK(constructed_term == expected_term);
+
+    // Check of division expression with signed operands
+    const auto constructed_term_signed =
+      convert_expr_to_smt(div_exprt{one_bvint, two_bvint});
+    const auto expected_term_signed =
+      smt_bit_vector_theoryt::signed_divide(smt_term_one, smt_term_two);
+    CHECK(constructed_term_signed == expected_term_signed);
+  }
+
+  SECTION(
+    "Ensure that division node conversion fails if the operands are not "
+    "bit-vector based")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(convert_expr_to_smt(div_exprt{one_bvint, false_exprt{}}));
+  }
+
+  SECTION(
+    "Remainder (modulus) from truncating division of two constant "
+    "size bit-vectors")
+  {
+    // Remainder expression with unsigned operands.
+    const auto constructed_term =
+      convert_expr_to_smt(mod_exprt{one_bvint_unsigned, two_bvint_unsigned});
+    const auto expected_term =
+      smt_bit_vector_theoryt::unsigned_remainder(smt_term_one, smt_term_two);
+    CHECK(constructed_term == expected_term);
+
+    // Remainder expression with signed operands
+    const auto constructed_term_signed =
+      convert_expr_to_smt(mod_exprt{one_bvint, two_bvint});
+    const auto expected_term_signed =
+      smt_bit_vector_theoryt::signed_remainder(smt_term_one, smt_term_two);
+    CHECK(constructed_term_signed == expected_term_signed);
+  }
+
+  SECTION(
+    "Ensure that remainder (truncated modulo) node conversion fails if the "
+    "operands are not bit-vector based")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(convert_expr_to_smt(mod_exprt{one_bvint, false_exprt{}}));
+  }
+
+  SECTION("Unary minus of constant size bit-vector")
+  {
+    const auto constructed_term =
+      convert_expr_to_smt(unary_minus_exprt{one_bvint});
+    const auto expected_term = smt_bit_vector_theoryt::negate(smt_term_one);
+    CHECK(constructed_term == expected_term);
+  }
+
+  SECTION(
+    "Ensure that unary minus node conversion fails if the operand is not a "
+    "bit-vector")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(convert_expr_to_smt(unary_minus_exprt{true_exprt{}}));
+  }
+}
diff --git a/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp b/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp
index 3f0207c8857..dbfb5d678b7 100644
--- a/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp
+++ b/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp
@@ -166,3 +166,162 @@ TEST_CASE("SMT bit vector predicates", "[core][smt2_incremental]")
       smt_bit_vector_theoryt::signed_greater_than_or_equal(two, wider));
   }
 }
+
+TEST_CASE(
+  "SMT bit vector arithmetic operator implementation tests",
+  "[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 four{4, 16};
+  const smt_bool_literal_termt true_val{true};
+
+  SECTION("Addition")
+  {
+    const auto function_application = smt_bit_vector_theoryt::add(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvadd", 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;
+    // Bit-vectors of mismatched sorts are going to hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::add(three, four));
+    // An addition of a bool and a bitvector should hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::add(three, true_val));
+  }
+
+  SECTION("Subtraction")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::subtract(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvsub", 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;
+    // Bit-vectors of mismatched sorts are going to hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::subtract(three, four));
+    // A subtraction of a bool and a bitvector should hit an
+    // invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::subtract(true_val, three));
+  }
+
+  SECTION("Multiplication")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::multiply(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvmul", 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;
+    // Bit-vectors of mismatched sorts are going to hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::multiply(three, four));
+    // A multiplication of a bool and a bitvector should hit an
+    // invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::multiply(true_val, three));
+  }
+
+  SECTION("Unsigned Division")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::unsigned_divide(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvudiv", 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;
+    // Bit-vectors of mismatched sorts are going to hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::unsigned_divide(three, four));
+    // A division of a bool and a bitvector should hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::unsigned_divide(true_val, three));
+  }
+
+  SECTION("Signed Division")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::signed_divide(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvsdiv", 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;
+    // Bit-vectors of mismatched sorts are going to hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::signed_divide(three, four));
+    // A division of a bool and a bitvector should hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::signed_divide(true_val, three));
+  }
+
+  SECTION("Unsigned Remainder")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::unsigned_remainder(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvurem", 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;
+    // Bit-vectors of mismatched sorts are going to hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::unsigned_remainder(three, four));
+    // A remainder of a bool and a bitvector should hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::unsigned_remainder(true_val, three));
+  }
+
+  SECTION("Signed Remainder")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::signed_remainder(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvsrem", 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;
+    // Bit-vectors of mismatched sorts are going to hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::signed_remainder(three, four));
+    // A remainder of a bool and a bitvector should hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::signed_remainder(true_val, three));
+  }
+
+  SECTION("Unary Minus")
+  {
+    const auto function_application = smt_bit_vector_theoryt::negate(two);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvneg", 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;
+    // Negation of a value of bool sort should fail with an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::negate(true_val));
+  }
+}