Add namespace access to smt2_incremental_decision_proceduret

So that instances of `symbol_exprt` can be handled correctly.

Author: thomasspriggs

src/goto-checker/solver_factory.cpp

@@ -333,7 +333,7 @@ solver_factoryt::get_incremental_smt2(std::string solver_command)
 
   return util_make_unique<solvert>(
     util_make_unique<smt2_incremental_decision_proceduret>(
-      std::move(solver_command), message_handler));
+      ns, std::move(solver_command), message_handler));
 }
 
 std::unique_ptr<solver_factoryt::solvert>

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -5,12 +5,15 @@
 #include <solvers/smt2_incremental/smt_commands.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
 #include <util/expr.h>
+#include <util/namespace.h>
 #include <util/string_utils.h>
 
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
+  const namespacet &_ns,
   std::string _solver_command,
   message_handlert &message_handler)
-  : solver_command(std::move(_solver_command)),
+  : ns{_ns},
+    solver_command(std::move(_solver_command)),
     number_of_solver_calls{0},
     solver_process{split_string(solver_command, ' ', false, true)},
     log{message_handler}

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -12,16 +12,20 @@
 
 class smt_commandt;
 class message_handlert;
+class namespacet;
 
 class smt2_incremental_decision_proceduret final
   : public stack_decision_proceduret
 {
 public:
+  /// \param _ns: Namespace for looking up the expressions which symbol_exprts
+  ///   relate to.
   /// \param solver_command:
   ///   The command and arguments for invoking the smt2 solver.
   /// \param message_handler:
   ///   The messaging system to be used for logging purposes.
   explicit smt2_incremental_decision_proceduret(
+    const namespacet &_ns,
     std::string solver_command,
     message_handlert &message_handler);
 
@@ -45,6 +49,8 @@ class smt2_incremental_decision_proceduret final
   ///    solver process.
   void send_to_solver(const smt_commandt &command);
 
+  const namespacet &ns;
+
   /// This is where we store the solver command for reporting the solver used.
   std::string solver_command;
   size_t number_of_solver_calls;