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$

src/solvers/smt2/smt2_conv.cpp

@@ -176,55 +176,55 @@ void smt2_convt::write_header()
     out << "(set-logic " << logic << ")" << "\n";
 }
 
-void smt2_convt::write_footer(std::ostream &os)
+void smt2_convt::write_footer()
 {
-  os << "\n";
+  out << "\n";
 
   // fix up the object sizes
   for(const auto &object : object_sizes)
     define_object_size(object.second, object.first);
 
   if(use_check_sat_assuming && !assumptions.empty())
   {
-    os << "(check-sat-assuming (";
+    out << "(check-sat-assuming (";
     for(const auto &assumption : assumptions)
       convert_literal(to_literal_expr(assumption).get_literal());
-    os << "))\n";
+    out << "))\n";
   }
   else
   {
     // add the assumptions, if any
     if(!assumptions.empty())
     {
-      os << "; assumptions\n";
+      out << "; assumptions\n";
 
       for(const auto &assumption : assumptions)
       {
-        os << "(assert ";
+        out << "(assert ";
         convert_literal(to_literal_expr(assumption).get_literal());
-        os << ")"
-           << "\n";
+        out << ")"
+            << "\n";
       }
     }
 
-    os << "(check-sat)\n";
+    out << "(check-sat)\n";
   }
 
-  os << "\n";
+  out << "\n";
 
   if(solver!=solvert::BOOLECTOR)
   {
     for(const auto &id : smt2_identifiers)
-      os << "(get-value (|" << id << "|))"
-         << "\n";
+      out << "(get-value (|" << id << "|))"
+          << "\n";
   }
 
-  os << "\n";
+  out << "\n";
 
-  os << "(exit)\n";
+  out << "(exit)\n";
 
-  os << "; end of SMT2 file"
-     << "\n";
+  out << "; end of SMT2 file"
+      << "\n";
 }
 
 void smt2_convt::define_object_size(
@@ -267,7 +267,7 @@ void smt2_convt::define_object_size(
 
 decision_proceduret::resultt smt2_convt::dec_solve()
 {
-  write_footer(out);
+  write_footer();
   out.flush();
   return decision_proceduret::resultt::D_ERROR;
 }

src/solvers/smt2/smt2_conv.h

@@ -96,7 +96,7 @@ class smt2_convt : public stack_decision_proceduret
   resultt dec_solve() override;
 
   void write_header();
-  void write_footer(std::ostream &);
+  void write_footer();
 
   // tweaks for arrays
   bool use_array_theory(const exprt &);

src/solvers/smt2/smt2_dec.cpp

@@ -39,13 +39,15 @@ decision_proceduret::resultt smt2_dect::dec_solve()
     temp_file_stdout("smt2_dec_stdout_", ""),
     temp_file_stderr("smt2_dec_stderr_", "");
 
-  {
-    // we write the problem into a file
-    std::ofstream problem_out(
-      temp_file_problem(), std::ios_base::out | std::ios_base::trunc);
-    problem_out << stringstream.str();
-    write_footer(problem_out);
-  }
+  const auto write_problem_to_file = [&](std::ofstream problem_out) {
+    cached_output << stringstream.str();
+    stringstream.str(std::string{});
+    write_footer();
+    problem_out << cached_output.str() << stringstream.str();
+    stringstream.str(std::string{});
+  };
+  write_problem_to_file(std::ofstream(
+    temp_file_problem(), std::ios_base::out | std::ios_base::trunc));
 
   std::vector<std::string> argv;
   std::string stdin_filename;

src/solvers/smt2/smt2_dec.h

@@ -45,6 +45,10 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt
 protected:
   message_handlert &message_handler;
 
+  /// Everything except the footer is cached, so that output files can be
+  /// rewritten with varying footers.
+  std::stringstream cached_output;
+
   resultt read_result(std::istream &in);
 };