Add doxygen of smt_convt::write_footer

This is worth explaining because it is no longer clear where the output
is written to based on the arguments/usage.

Author: thomasspriggs

src/solvers/smt2/smt2_conv.h

@@ -96,6 +96,15 @@ class smt2_convt : public stack_decision_proceduret
   resultt dec_solve() override;
 
   void write_header();
+  /// Writes the end of the SMT file to the `smt_convt::out` stream. These parts
+  /// of the output may be changed when using multiple rounds of solving. They
+  /// include the following parts of the output file -
+  ///  * The object size definitions.
+  ///  * The assertions based on the `assumptions` member variable.
+  ///  * The `(check-sat)` or `check-sat-assuming` command.
+  ///  * A `(get-value |identifier|)` command for each of the identifiers in
+  ///    `smt2_convt::smt2_identifiers`.
+  ///  * An `(exit)` command.
   void write_footer();
 
   // tweaks for arrays