Restore namespace after symbolic execution

This was already fixed in d475abc, but 685937a introduced additional
returns. Now use an approach that will always work, even when returning via
exceptions being thrown.

Author: tautschnig

regression/cbmc/coverage_report1/paths.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--symex-coverage-report - --paths lifo
+<line branch="false" hits="1" number="12"/>
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-symex/symex_main.cpp

@@ -242,12 +242,32 @@ void goto_symext::symex_with_state(
   const get_goto_functiont &get_goto_function,
   symbol_tablet &new_symbol_table)
 {
+  struct reset_namespacet
+  {
+    explicit reset_namespacet(namespacet &ns)
+      : ns(ns)
+    {
+    }
+
+    ~reset_namespacet()
+    {
+      const symbol_tablet &st = ns.get_symbol_table();
+      ns = namespacet(st);
+    }
+
+    namespacet &ns;
+  };
+
   // We'll be using ns during symbolic execution and it needs to know
   // about the names minted in `state`, so make it point both to
   // `state`'s symbol table and the symbol table of the original
   // goto-program.
   ns = namespacet(outer_symbol_table, state.symbol_table);
 
+  // whichever way we exit this method, reset the namespace back to a sane state
+  // as state.symbol_table might go out of scope
+  reset_namespacet reset_ns(ns);
+
   PRECONDITION(state.top().end_of_function->is_end_function());
 
   symex_threaded_step(state, get_goto_function);
@@ -267,9 +287,6 @@ void goto_symext::symex_with_state(
   // execution, so return the names generated through symbolic execution
   // through `new_symbol_table`.
   new_symbol_table = state.symbol_table;
-  // reset the namespace back to a sane state as state.symbol_table might go out
-  // of scope
-  ns = namespacet(outer_symbol_table);
 }
 
 void goto_symext::resume_symex_from_saved_state(