diff --git a/src/solvers/smt2_incremental/object_tracking.h b/src/solvers/smt2_incremental/object_tracking.h
index 24563e7abd2..15403e50447 100644
--- a/src/solvers/smt2_incremental/object_tracking.h
+++ b/src/solvers/smt2_incremental/object_tracking.h
@@ -40,7 +40,7 @@
 struct decision_procedure_objectt
 {
   /// The expression for the root of the object. This is expression equivalent
-  /// to deferencing a pointer to this object with a zero offset.
+  /// to dereferencing a pointer to this object with a zero offset.
   exprt base_expression;
   /// Number which uniquely identifies this particular object.
   std::size_t unique_id = 0;
@@ -57,7 +57,7 @@ struct decision_procedure_objectt
 /// assigned.
 exprt find_object_base_expression(const address_of_exprt &address_of);
 
-/// Arbitary expressions passed to the decision procedure may have multiple
+/// Arbitrary expressions passed to the decision procedure may have multiple
 /// address of operations as its sub expressions. This means the overall
 /// expression may contain multiple base objects which need to be assigned
 /// unique identifiers.
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 16b26ce3a3f..071b469f91c 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -40,6 +40,8 @@ static smt_responset get_response_to_command(
     return response;
 }
 
+/// Returns a message string describing the problem in the case where the
+/// response from the solver is an error status. Returns empty otherwise.
 static optionalt<std::string>
 get_problem_messages(const smt_responset &response)
 {
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
index 36eaba4da64..7dcc0278e95 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -94,6 +94,9 @@ class smt2_incremental_decision_proceduret final
   /// \brief Defines any functions which \p expr depends on, which have not yet
   ///   been defined, along with their dependencies in turn.
   void define_dependent_functions(const exprt &expr);
+  /// If a function has not been defined for handling \p expr, then a new
+  /// function is defined. If the corresponding function exists already, then
+  /// no action is taken.
   void ensure_handle_for_expr_defined(const exprt &expr);
   /// \brief Add objects in \p expr to object_map if needed and convert to smt.
   /// \note This function is non-const because it mutates the object_map.