Solver factory shouldn't have its own namespacet instance

The namespace is passed on into the solver allocated.
If the solver factory goes out of scope then the solver
will crash.

Author: peterschrammel

src/cbmc/bmc.cpp

@@ -276,6 +276,7 @@ int bmct::do_language_agnostic_bmc(
   safety_checkert::resultt final_result = safety_checkert::resultt::SAFE;
   safety_checkert::resultt tmp_result = safety_checkert::resultt::SAFE;
   const symbol_tablet &symbol_table = model.get_symbol_table();
+  namespacet ns(symbol_table);
   messaget message(ui);
   std::unique_ptr<path_storaget> worklist;
   std::string strategy = opts.get_option("exploration-strategy");
@@ -285,12 +286,10 @@ int bmct::do_language_agnostic_bmc(
   worklist = path_strategy_chooser.get(strategy);
   try
   {
+    solver_factoryt solvers(
+      opts, ns, ui, ui.get_ui() == ui_message_handlert::uit::XML_UI);
+
     {
-      solver_factoryt solvers(
-        opts,
-        symbol_table,
-        ui,
-        ui.get_ui() == ui_message_handlert::uit::XML_UI);
       std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
         solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
@@ -333,11 +332,6 @@ int bmct::do_language_agnostic_bmc(
 
     while(!worklist->empty())
     {
-      solver_factoryt solvers(
-        opts,
-        symbol_table,
-        ui,
-        ui.get_ui() == ui_message_handlert::uit::XML_UI);
       std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
         solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();

src/goto-checker/solver_factory.cpp

@@ -18,7 +18,6 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/options.h>
-#include <util/symbol_table.h>
 #include <util/version.h>
 
 #ifdef _MSC_VER
@@ -35,12 +34,11 @@ Author: Daniel Kroening, Peter Schrammel
 
 solver_factoryt::solver_factoryt(
   const optionst &_options,
-  const symbol_tablet &_symbol_table,
+  const namespacet &_ns,
   message_handlert &_message_handler,
   bool _output_xml_in_refinement)
   : options(_options),
-    symbol_table(_symbol_table),
-    ns(_symbol_table),
+    ns(_ns),
     message_handler(_message_handler),
     output_xml_in_refinement(_output_xml_in_refinement)
 {

src/goto-checker/solver_factory.h

@@ -21,14 +21,14 @@ class namespacet;
 class optionst;
 class propt;
 class prop_convt;
-class symbol_tablet;
 
 class solver_factoryt
 {
 public:
+  /// Note: The solver returned will hold a reference to the namespace `ns`.
   solver_factoryt(
     const optionst &_options,
-    const symbol_tablet &_symbol_table,
+    const namespacet &_ns,
     message_handlert &_message_handler,
     bool _output_xml_in_refinement);
 
@@ -62,8 +62,7 @@ class solver_factoryt
 
 protected:
   const optionst &options;
-  const symbol_tablet &symbol_table;
-  namespacet ns;
+  const namespacet &ns;
   message_handlert &message_handler;
   const bool output_xml_in_refinement;
 

unit/path_strategies.cpp

@@ -377,9 +377,10 @@ void _check_with_strategy(
   ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, log, mh);
   REQUIRE(ret == -1);
 
-  solver_factoryt initial_solvers(opts, gm.get_symbol_table(), mh, false);
+  namespacet ns(gm.get_symbol_table());
+  solver_factoryt solver_factory(opts, ns, mh, false);
   std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
-    initial_solvers.get_solver();
+    solver_factory.get_solver();
   prop_convt &initial_pc = cbmc_solver->prop_conv();
   std::function<bool(void)> callback = []() { return false; };
 
@@ -404,8 +405,7 @@ void _check_with_strategy(
 
   while(!worklist->empty())
   {
-    solver_factoryt solvers(opts, gm.get_symbol_table(), mh, false);
-    cbmc_solver = solvers.get_solver();
+    cbmc_solver = solver_factory.get_solver();
     prop_convt &pc = cbmc_solver->prop_conv();
     path_storaget::patht &resume = worklist->peek();