Deduplicate output streams in smt2_convt::write_footer()

This fixes bugs arising from some of the member functions of
`smt2::convt` writing to an `os` argument and some of the them writing
to `smt2_convt::out`. This was causing some of the generated text to be
written out when using `--outfile` argument with cbmc, but not without
it.

It might be easier to understand `smt2_convt` if the output stream was
passed as an argument to the member functions, instead of kept as a
member variable. This commit replaces the arguments with references to
the member variable because it is a less wide sweeping change and it
still solves the bugs.

The address_space_size_limit3 test is disabled with smt2, because the
output of this test was already different between the sat and smt2
backends and therefore it was already not producing the correct output.
Presumably this test was returning the expected `VERIFICATION FAILED`
result for the wrong reasons. The `VERIFICATION FAILED` result is only
returned in the case where the object size limits are missing. Further
work will be needed to properly debug the support for `--pointer-check`
with smt2.

Author: thomasspriggs

regression/cbmc/Malloc6/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/Pointer1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/Pointer28/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --little-endian
 ^EXIT=0$

regression/cbmc/Pointer4/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/String8/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

regression/cbmc/String_Abstraction7/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --string-abstraction --pointer-check --bounds-check
 ^EXIT=0$

regression/cbmc/address_space_size_limit3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.i
 --32 --little-endian --object-bits 25 --pointer-check
 ^EXIT=10$

regression/cbmc/null7/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/struct7/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

regression/cbmc/void_pointer2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --no-simplify --unwind 3
 ^EXIT=0$